src/Pure/tactic.ML
changeset 23702 58ca991e0702
parent 23539 df5440e241a1
child 24244 d7ee11ba1534