equal
deleted
inserted
replaced
505 * Renamed some important ML structures, while keeping the old names as |
505 * Renamed some important ML structures, while keeping the old names as |
506 legacy aliases for some time: |
506 legacy aliases for some time: |
507 |
507 |
508 OuterKeyword ~> Keyword |
508 OuterKeyword ~> Keyword |
509 OuterParse ~> Parse |
509 OuterParse ~> Parse |
|
510 SpecParse ~> Parse_Spec |
510 |
511 |
511 |
512 |
512 *** System *** |
513 *** System *** |
513 |
514 |
514 * Discontinued special HOL_USEDIR_OPTIONS for the main HOL image; |
515 * Discontinued special HOL_USEDIR_OPTIONS for the main HOL image; |