src/Pure/tctical.ML
changeset 15307 10dd989282fd
parent 15017 9ad392226da5
child 15531 08c8dad8e399