src/HOL/thy_syntax.ML
changeset 3225 cee363fc07d7
parent 3194 36bfceef1800
child 3308 da002cef7090