src/HOL/thy_syntax.ML
changeset 12128 25565bbbd246
parent 12050 6934c005aec4
child 12180 91c9f661b183