src/Pure/tactic.ML
changeset 22234 52ba19aaa9c2
parent 21708 45e7491bea47
child 22360 26ead7ed4f4b