src/Pure/tctical.ML
changeset 15481 fc075ae929e4
parent 15017 9ad392226da5
child 15531 08c8dad8e399