src/HOL/thy_syntax.ML
changeset 3872 a5839ecee7b8
parent 3665 3b44fac767f6
child 3945 ae9c61d69888