src/HOL/thy_syntax.ML
changeset 6599 dc5bf3f40ad3
parent 6576 7e0b35bed503
child 6642 732af87c0650