src/Pure/General/symbol.ML
changeset 65958 6338355b2a88
parent 64275 ac2abc987cf9
child 66020 a31760eee09d
equal deleted inserted replaced
65956:639eb3617a86 65958:6338355b2a88