Def Mathlib.Tactic.onGoal

Modification history

2022-02-07 10:11
Mathlib/Tactic/PermuteGoals.lean
chore: drop `rotate_goals` tactic (#185) …
Deleted Mathlib.Tactic.onGoalView on Github →
2022-02-06 19:49
Mathlib/Tactic/PermuteGoals.lean
feat: `rotate_goals`, `pick_goal` and `swap` (#178) …
Added Mathlib.Tactic.onGoalView on Github →