src/Pure/tctical.ML
changeset 7020 75ff179df7b7
parent 6390 5d58c100ca3f
child 7686 4731f10af2e6
equal deleted inserted replaced
7019:71f2155cdd85 7020:75ff179df7b7