src/Pure/tactic.ML
changeset 24623 7b2bc73405b8
parent 24244 d7ee11ba1534
child 25939 ddea202704b4