src/HOL/thy_syntax.ML
changeset 3061 25b2a895f864
parent 2930 602cdeabb89b
child 3194 36bfceef1800