src/Pure/Syntax/syntax_phases.ML
changeset 58937 49e8115f70d8
parent 58047 9f3826352b52
child 58978 e42da880c61e