src/Pure/Syntax/syntax.ML
changeset 25456 6f79698f294d
parent 25394 db25c98f32e1
child 25476 03da46cfab9e