src/Pure/Syntax/syntax_phases.ML
changeset 66885 d3d508b23d1d
parent 64677 8dc24130e8fe
child 67507 5db077cfe1b2