changeset 37216 | 3165bc303f66 |
parent 37158 | c96e119b7fe9 |
child 37218 | ffd587207d5d |
--- a/NEWS Mon May 31 19:36:13 2010 +0200 +++ b/NEWS Mon May 31 21:06:57 2010 +0200 @@ -503,9 +503,12 @@ OuterLex ~> Token OuterParse ~> Parse OuterSyntax ~> Outer_Syntax + PrintMode ~> Print_Mode SpecParse ~> Parse_Spec + ThyInfo ~> Thy_Info + ThyLoad ~> Thy_Load + ThyOutput ~> Thy_Output TypeInfer ~> Type_Infer - PrintMode ~> Print_Mode Note that "open Legacy" simplifies porting of sources, but forgetting to remove it again will complicate porting again in the future.