src/HOL/thy_syntax.ML
changeset 4072 d0d32dd77440
parent 4032 4b1c69d8b767
child 4091 771b1f6422a8