src/Pure/Syntax/simple_syntax.ML
changeset 42889 412fe70f41a4
parent 42279 6da43a5018e2
child 46214 8534f949548e
equal deleted inserted replaced
42888:4da581400b69 42889:412fe70f41a4