src/Pure/Syntax/syntax_phases.ML
changeset 74300 33f13d2d211c
parent 74262 839a6e284545
child 74561 8e6c973003c8
equal deleted inserted replaced
74299:16e5870fe21e 74300:33f13d2d211c