src/Pure/tactic.ML
changeset 25286 35e954ff67f8
parent 24244 d7ee11ba1534
child 25939 ddea202704b4