misc updates for release;
authorwenzelm
Thu May 27 15:28:23 2010 +0200 (2010-05-27)
changeset 37144fd6308b4df72
parent 37143 2a5182751151
child 37145 01aa36932739
child 37154 f6ae8db23352
child 37169 f69efa106feb
misc updates for release;
CONTRIBUTORS
NEWS
     1.1 --- a/CONTRIBUTORS	Thu May 27 15:15:20 2010 +0200
     1.2 +++ b/CONTRIBUTORS	Thu May 27 15:28:23 2010 +0200
     1.3 @@ -3,17 +3,20 @@
     1.4  who is listed as an author in one of the source files of this Isabelle
     1.5  distribution.
     1.6  
     1.7 -Contributions to this Isabelle version
     1.8 +Contributions to Isabelle2009-2
     1.9  --------------------------------------
    1.10  
    1.11 -* April 2010, Florian Haftmann, TUM
    1.12 +* April 2010: Florian Haftmann, TUM
    1.13    Reorganization of abstract algebra type classes.
    1.14  
    1.15 -* April 2010, Florian Haftmann, TUM
    1.16 +* April 2010: Florian Haftmann, TUM
    1.17    Code generation for data representations involving invariants;
    1.18    various collections avaiable in theories Fset, Dlist, RBT,
    1.19    Mapping and AssocList.
    1.20  
    1.21 +* March 2010: Sascha Boehme, TUM
    1.22 +  Efficient SHA1 library for Poly/ML.
    1.23 +
    1.24  
    1.25  Contributions to Isabelle2009-1
    1.26  -------------------------------
     2.1 --- a/NEWS	Thu May 27 15:15:20 2010 +0200
     2.2 +++ b/NEWS	Thu May 27 15:28:23 2010 +0200
     2.3 @@ -1,8 +1,8 @@
     2.4  Isabelle NEWS -- history user-relevant changes
     2.5  ==============================================
     2.6  
     2.7 -New in this Isabelle version
     2.8 -----------------------------
     2.9 +New in Isabelle2009-2 (June 2010)
    2.10 +---------------------------------
    2.11  
    2.12  *** General ***
    2.13  
    2.14 @@ -146,9 +146,9 @@
    2.15  * List membership infix mem operation is only an input abbreviation.
    2.16  INCOMPATIBILITY.
    2.17  
    2.18 -* Theory Library/Word.thy has been removed.  Use library Word/Word.thy for
    2.19 -future developements;  former Library/Word.thy is still present in the AFP
    2.20 -entry RSAPPS.
    2.21 +* Theory Library/Word.thy has been removed.  Use library Word/Word.thy
    2.22 +for future developements; former Library/Word.thy is still present in
    2.23 +the AFP entry RSAPPS.
    2.24  
    2.25  * Theorem Int.int_induct renamed to Int.int_of_nat_induct and is no
    2.26  longer shadowed.  INCOMPATIBILITY.
    2.27 @@ -197,7 +197,7 @@
    2.28    ceiling_subtract_number_of ~> ceiling_diff_number_of
    2.29    ceiling_subtract_one       ~> ceiling_diff_one
    2.30  
    2.31 -* Theory 'Finite_Set': various folding_XXX locales facilitate the
    2.32 +* Theory "Finite_Set": various folding_XXX locales facilitate the
    2.33  application of the various fold combinators on finite sets.
    2.34  
    2.35  * Library theory "RBT" renamed to "RBT_Impl"; new library theory "RBT"
    2.36 @@ -494,13 +494,28 @@
    2.37  
    2.38  *** ML ***
    2.39  
    2.40 -* Sorts.certify_sort and derived "cert" operations for types and terms
    2.41 -no longer minimize sorts.  Thus certification at the boundary of the
    2.42 -inference kernel becomes invariant under addition of class relations,
    2.43 -which is an important monotonicity principle.  Sorts are now minimized
    2.44 -in the syntax layer only, at the boundary between the end-user and the
    2.45 -system.  Subtle INCOMPATIBILITY, may have to use Sign.minimize_sort
    2.46 -explicitly in rare situations.
    2.47 +* Renamed some important ML structures, while keeping the old names
    2.48 +for some time as aliases within the structure Legacy:
    2.49 +
    2.50 +  OuterKeyword  ~>  Keyword
    2.51 +  OuterLex      ~>  Token
    2.52 +  OuterParse    ~>  Parse
    2.53 +  OuterSyntax   ~>  Outer_Syntax
    2.54 +  SpecParse     ~>  Parse_Spec
    2.55 +
    2.56 +Note that "open Legacy" simplifies porting of sources, but forgetting
    2.57 +to remove it again will complicate porting again in the future.
    2.58 +
    2.59 +* Most operations that refer to a global context are named
    2.60 +accordingly, e.g. Simplifier.global_context or
    2.61 +ProofContext.init_global.  There are some situations where a global
    2.62 +context actually works, but under normal circumstances one needs to
    2.63 +pass the proper local context through the code!
    2.64 +
    2.65 +* Discontinued old TheoryDataFun with its copy/init operation -- data
    2.66 +needs to be pure.  Functor Theory_Data_PP retains the traditional
    2.67 +Pretty.pp argument to merge, which is absent in the standard
    2.68 +Theory_Data version.
    2.69  
    2.70  * Antiquotations for basic formal entities:
    2.71  
    2.72 @@ -523,21 +538,21 @@
    2.73  values similar to the ML toplevel.  The result is compiler dependent
    2.74  and may fall back on "?" in certain situations.
    2.75  
    2.76 +* Sorts.certify_sort and derived "cert" operations for types and terms
    2.77 +no longer minimize sorts.  Thus certification at the boundary of the
    2.78 +inference kernel becomes invariant under addition of class relations,
    2.79 +which is an important monotonicity principle.  Sorts are now minimized
    2.80 +in the syntax layer only, at the boundary between the end-user and the
    2.81 +system.  Subtle INCOMPATIBILITY, may have to use Sign.minimize_sort
    2.82 +explicitly in rare situations.
    2.83 +
    2.84  * Renamed old-style Drule.standard to Drule.export_without_context, to
    2.85  emphasize that this is in no way a standard operation.
    2.86  INCOMPATIBILITY.
    2.87  
    2.88 -* Curried take and drop in library.ML; negative length is interpreted
    2.89 -as infinity (as in chop).  INCOMPATIBILITY.
    2.90 -
    2.91  * Subgoal.FOCUS (and variants): resulting goal state is normalized as
    2.92  usual for resolution.  Rare INCOMPATIBILITY.
    2.93  
    2.94 -* Discontinued old TheoryDataFun with its copy/init operation -- data
    2.95 -needs to be pure.  Functor Theory_Data_PP retains the traditional
    2.96 -Pretty.pp argument to merge, which is absent in the standard
    2.97 -Theory_Data version.
    2.98 -
    2.99  * Renamed varify/unvarify operations to varify_global/unvarify_global
   2.100  to emphasize that these only work in a global situation (which is
   2.101  quite rare).
   2.102 @@ -545,23 +560,11 @@
   2.103  * Configuration options now admit dynamic default values, depending on
   2.104  the context or even global references.
   2.105  
   2.106 -* Most operations that refer to a global context are named
   2.107 -accordingly, e.g. Simplifier.global_context or
   2.108 -ProofContext.init_global.  There are some situations where a global
   2.109 -context actually works, but under normal circumstances one needs to
   2.110 -pass the proper local context through the code!
   2.111 -
   2.112 -* Renamed some important ML structures, while keeping the old names
   2.113 -for some time as aliases within the structure Legacy:
   2.114 -
   2.115 -  OuterKeyword  ~>  Keyword
   2.116 -  OuterLex      ~>  Token
   2.117 -  OuterParse    ~>  Parse
   2.118 -  OuterSyntax   ~>  Outer_Syntax
   2.119 -  SpecParse     ~>  Parse_Spec
   2.120 -
   2.121 -Note that "open Legacy" simplifies porting of sources, but forgetting
   2.122 -to remove it again will complicate porting again in the future.
   2.123 +* SHA1.digest digests strings according to SHA-1 (see RFC 3174).  It
   2.124 +uses an efficient external library if available (for Poly/ML).
   2.125 +
   2.126 +* Curried take and drop in library.ML; negative length is interpreted
   2.127 +as infinity (as in chop).  Subtle INCOMPATIBILITY.
   2.128  
   2.129  
   2.130  *** System ***