src/HOL/thy_syntax.ML
changeset 6059 aa00e235ea27
parent 6035 c041fc54ab4c
child 6103 36f272ea9413
equal deleted inserted replaced
6058:a9600c47ace3 6059:aa00e235ea27