src/HOL/thy_syntax.ML
changeset 3729 6be7cf5086ab
parent 3665 3b44fac767f6
child 3945 ae9c61d69888
equal deleted inserted replaced
3728:f92594f65af6 3729:6be7cf5086ab