src/HOL/thy_syntax.ML
changeset 12125 316d11f760f7
parent 12050 6934c005aec4
child 12180 91c9f661b183