src/Pure/tctical.ML
changeset 14379 ea10a8c3e9cf
parent 13664 cfe1dc32c2e5
child 15006 107e4dfd3b96