src/Pure/Syntax/ROOT.ML
changeset 2003 b48f066d52dc
parent 1506 192c48376d25
child 2198 0dddd9575717
equal deleted inserted replaced
2002:ed423882c6a9 2003:b48f066d52dc