src/Pure/tactic.ML
changeset 68213 bb93511c7e8f
parent 67721 5348bea4accd
child 68825 8207c67d9ef4