src/Pure/Syntax/syntax_phases.ML
changeset 43576 ebeda6275027
parent 43552 156c822f181a
child 43731 70072780e095
equal deleted inserted replaced
43575:cfb2077cb2db 43576:ebeda6275027