src/Pure/tactic.ML
changeset 23597 ab67175ca8a5
parent 23539 df5440e241a1
child 24244 d7ee11ba1534
equal deleted inserted replaced
23596:f8381a95c49c 23597:ab67175ca8a5