src/HOL/thy_syntax.ML
changeset 4208 b67223fddc11
parent 4204 7b15e7eee982
child 4225 3d9e551bc5a6
equal deleted inserted replaced
4207:061919f8da9c 4208:b67223fddc11