src/Pure/tactic.ML
changeset 24208 f4cafbaa05e4
parent 23539 df5440e241a1
child 24244 d7ee11ba1534