src/Pure/tactic.ML
changeset 68344 3bb44c25ce8b
parent 67721 5348bea4accd
child 68825 8207c67d9ef4