src/Pure/tactic.ML
changeset 35640 9617aeca7147
parent 35611 07a8904f8fcd
child 36354 bbd742107f56