src/Pure/Thy/thy_syntax.ML
changeset 44574 24444588fddd
parent 44354 88bf93c2ae7c
child 44658 5bec9c15ef29
equal deleted inserted replaced
44573:51f8895b9ad9 44574:24444588fddd