src/Pure/tactic.ML
changeset 22324 c95319d14332
parent 21708 45e7491bea47
child 22360 26ead7ed4f4b