src/Pure/tctical.ML
changeset 15517 3bc57d428ec1
parent 15017 9ad392226da5
child 15531 08c8dad8e399