src/HOL/thy_syntax.ML
changeset 12207 4dff931b852f
parent 12180 91c9f661b183
child 12505 46bfc675015a