src/Pure/Syntax/syntax_phases.ML
changeset 72794 3757e64e75bb
parent 71675 55cb4271858b
child 73163 624c2b98860a