src/HOL/thy_syntax.ML
changeset 1072 0140ff702b23
parent 977 5d57287e5e1e
child 1251 81fc4d8e3eda