src/Pure/tactic.ML
changeset 33028 9aa8bfb1649d
parent 32971 55ba9b6648ef
child 33955 fff6f11b1f09