src/Pure/tctical.ML
changeset 23597 ab67175ca8a5
parent 23584 9b5ba76de1c2
child 23922 707639e9497d
equal deleted inserted replaced
23596:f8381a95c49c 23597:ab67175ca8a5