src/Pure/tctical.ML
changeset 30126 332e739b6b0e
parent 29272 fb3ccf499df5
child 30145 09817540ccae
equal deleted inserted replaced
30124:b956bf0dc87c 30126:332e739b6b0e