src/Pure/tctical.ML
changeset 29554 7e5e5ebb7bf7
parent 29272 fb3ccf499df5
child 30145 09817540ccae
equal deleted inserted replaced
29553:c3b937e8597b 29554:7e5e5ebb7bf7