src/Pure/Syntax/syntax_phases.ML
changeset 58668 1891f17c6124
parent 58047 9f3826352b52
child 58978 e42da880c61e
equal deleted inserted replaced
58667:d2a7b443ceb2 58668:1891f17c6124