src/HOL/thy_syntax.ML
changeset 2981 aa5aeb6467c6
parent 2930 602cdeabb89b
child 3194 36bfceef1800