NEWS
changeset 5251 fee54d5c511c
parent 5226 89934cd022a9
child 5267 41a01176b9de
     1.1 --- a/NEWS	Tue Aug 04 18:40:18 1998 +0200
     1.2 +++ b/NEWS	Tue Aug 04 18:41:11 1998 +0200
     1.3 @@ -241,25 +241,27 @@
     1.4  
     1.5  *** Internal programming interfaces ***
     1.6  
     1.7 -* removed global_names compatibility flag -- all theory declarations
     1.8 -are qualified by default;
     1.9 +* Pure: several new basic modules made available for general use, see
    1.10 +also src/Pure/README;
    1.11  
    1.12  * improved the theory data mechanism to support encapsulation (data
    1.13  kind name replaced by private Object.kind, acting as authorization
    1.14  key); new type-safe user interface via functor TheoryDataFun;
    1.15  
    1.16 +* removed global_names compatibility flag -- all theory declarations
    1.17 +are qualified by default;
    1.18 +
    1.19  * module Pure/Syntax now offers quote / antiquote translation
    1.20  functions (useful for Hoare logic etc. with implicit dependencies);
    1.21  
    1.22  * Simplifier now offers conversions (asm_)(full_)rewrite: simpset ->
    1.23  cterm -> thm;
    1.24  
    1.25 -* Pure: several new basic modules made available for general use, see
    1.26 -also src/Pure/README;
    1.27 -
    1.28  * new tactical CHANGED_GOAL for checking that a tactic modifies a
    1.29  subgoal;
    1.30  
    1.31 +* Display.print_goals function moved to Locale.print_goals;
    1.32 +
    1.33  
    1.34  
    1.35  New in Isabelle98 (January 1998)