src/Pure/tctical.ML
changeset 16352 d7f9978e5752
parent 16179 fa7e70be26b0
child 16510 606d919ad3c3