src/HOL/thy_syntax.ML
changeset 3362 0b268cff9344
parent 3345 4d888ddd6284
child 3403 6cc663f6d62e
equal deleted inserted replaced
3361:1877e333f66c 3362:0b268cff9344