src/Pure/tactic.ML
changeset 23719 ccd9cb15c062
parent 23539 df5440e241a1
child 24244 d7ee11ba1534