src/HOL/thy_syntax.ML
changeset 3015 65778b9d865f
parent 2930 602cdeabb89b
child 3194 36bfceef1800