src/Pure/tactic.ML
changeset 60916 a6e2a667b0a8
parent 60793 bbcd4ab6d26e
child 67721 5348bea4accd