src/Pure/Syntax/syntax.ML
changeset 18208 dbdcf366db53
parent 17496 26535df536ae
child 18428 4059413acbc1