src/Pure/tactic.ML
changeset 22264 6a65e9b2ae05
parent 21708 45e7491bea47
child 22360 26ead7ed4f4b