src/HOL/thy_syntax.ML
changeset 3895 b2463861c86a
parent 3665 3b44fac767f6
child 3945 ae9c61d69888