src/HOL/thy_syntax.ML
changeset 3729 6be7cf5086ab
parent 3665 3b44fac767f6
child 3945 ae9c61d69888