src/Pure/tactic.ML
changeset 24547 64c20ee76bc1
parent 24244 d7ee11ba1534
child 25939 ddea202704b4