src/Pure/tactic.ML
changeset 1444 23ceb1dc9755
parent 1209 03dc596b3a18
child 1458 fd510875fb71