src/Pure/tctical.ML
changeset 16319 1ff2965cc2e7
parent 16179 fa7e70be26b0
child 16510 606d919ad3c3