src/Pure/tactic.ML
changeset 10416 5b33e732e459
parent 10415 e6d7b77a0574
child 10444 2dfa19236768