src/Pure/tactic.ML
changeset 33037 b22e44496dc2
parent 32971 55ba9b6648ef
child 33955 fff6f11b1f09