src/Pure/Syntax/syntax_phases.ML
changeset 73503 eda1d95ef538
parent 73163 624c2b98860a
child 73686 b9aae426e51d