src/Pure/tctical.ML
changeset 30838 d09a0794d457
parent 30145 09817540ccae
child 31945 d5f186aa0bed
equal deleted inserted replaced
30836:1344132160bb 30838:d09a0794d457