src/Pure/tactic.ML
changeset 1228 7d6b0241afab
parent 1209 03dc596b3a18
child 1458 fd510875fb71