src/Pure/tctical.ML
changeset 15517 3bc57d428ec1
parent 15017 9ad392226da5
child 15531 08c8dad8e399
equal deleted inserted replaced
15516:a4bbed7487ea 15517:3bc57d428ec1