equal
deleted
inserted
replaced
501 |
501 |
502 OuterKeyword ~> Keyword |
502 OuterKeyword ~> Keyword |
503 OuterLex ~> Token |
503 OuterLex ~> Token |
504 OuterParse ~> Parse |
504 OuterParse ~> Parse |
505 OuterSyntax ~> Outer_Syntax |
505 OuterSyntax ~> Outer_Syntax |
|
506 PrintMode ~> Print_Mode |
506 SpecParse ~> Parse_Spec |
507 SpecParse ~> Parse_Spec |
|
508 ThyInfo ~> Thy_Info |
|
509 ThyLoad ~> Thy_Load |
|
510 ThyOutput ~> Thy_Output |
507 TypeInfer ~> Type_Infer |
511 TypeInfer ~> Type_Infer |
508 PrintMode ~> Print_Mode |
|
509 |
512 |
510 Note that "open Legacy" simplifies porting of sources, but forgetting |
513 Note that "open Legacy" simplifies porting of sources, but forgetting |
511 to remove it again will complicate porting again in the future. |
514 to remove it again will complicate porting again in the future. |
512 |
515 |
513 * Most operations that refer to a global context are named |
516 * Most operations that refer to a global context are named |