src/Pure/tactic.ML
changeset 68115 23c6ae3dd3a0
parent 67721 5348bea4accd
child 68825 8207c67d9ef4
equal deleted inserted replaced
68114:ce7f35406f37 68115:23c6ae3dd3a0