src/Pure/tactic.ML
changeset 33020 0908ed080ccf
parent 32971 55ba9b6648ef
child 33955 fff6f11b1f09