src/Pure/Syntax/syntax_phases.ML
changeset 56812 baef1c110f12
parent 56334 6b3739fee456
child 58047 9f3826352b52