src/HOL/thy_syntax.ML
changeset 3362 0b268cff9344
parent 3345 4d888ddd6284
child 3403 6cc663f6d62e