src/Pure/tactic.ML
changeset 25456 6f79698f294d
parent 24244 d7ee11ba1534
child 25939 ddea202704b4