src/Pure/tctical.ML
changeset 30227 853abb4853cc
parent 30145 09817540ccae
child 31945 d5f186aa0bed
equal deleted inserted replaced
30226:2f4684e2ea95 30227:853abb4853cc