src/Pure/Syntax/simple_syntax.ML
changeset 43004 20e9caff1f86
parent 42279 6da43a5018e2
child 46214 8534f949548e
equal deleted inserted replaced
43003:5a86009366fc 43004:20e9caff1f86