src/Pure/tactic.ML
changeset 4212 68c7b37f8721
parent 4178 e64ff1c1bc70
child 4213 cef5ef41e70d