src/Pure/tactic.ML
changeset 25111 d52a58b51f1f
parent 24244 d7ee11ba1534
child 25939 ddea202704b4