--- a/CONTRIBUTORS Thu May 27 16:29:33 2010 +0200
+++ b/CONTRIBUTORS Thu May 27 16:30:26 2010 +0200
@@ -3,17 +3,20 @@
who is listed as an author in one of the source files of this Isabelle
distribution.
-Contributions to this Isabelle version
+Contributions to Isabelle2009-2
--------------------------------------
-* April 2010, Florian Haftmann, TUM
+* April 2010: Florian Haftmann, TUM
Reorganization of abstract algebra type classes.
-* April 2010, Florian Haftmann, TUM
+* April 2010: Florian Haftmann, TUM
Code generation for data representations involving invariants;
various collections avaiable in theories Fset, Dlist, RBT,
Mapping and AssocList.
+* March 2010: Sascha Boehme, TUM
+ Efficient SHA1 library for Poly/ML.
+
Contributions to Isabelle2009-1
-------------------------------
--- a/NEWS Thu May 27 16:29:33 2010 +0200
+++ b/NEWS Thu May 27 16:30:26 2010 +0200
@@ -1,8 +1,8 @@
Isabelle NEWS -- history user-relevant changes
==============================================
-New in this Isabelle version
-----------------------------
+New in Isabelle2009-2 (June 2010)
+---------------------------------
*** General ***
@@ -146,9 +146,9 @@
* List membership infix mem operation is only an input abbreviation.
INCOMPATIBILITY.
-* Theory Library/Word.thy has been removed. Use library Word/Word.thy for
-future developements; former Library/Word.thy is still present in the AFP
-entry RSAPPS.
+* Theory Library/Word.thy has been removed. Use library Word/Word.thy
+for future developements; former Library/Word.thy is still present in
+the AFP entry RSAPPS.
* Theorem Int.int_induct renamed to Int.int_of_nat_induct and is no
longer shadowed. INCOMPATIBILITY.
@@ -197,7 +197,7 @@
ceiling_subtract_number_of ~> ceiling_diff_number_of
ceiling_subtract_one ~> ceiling_diff_one
-* Theory 'Finite_Set': various folding_XXX locales facilitate the
+* Theory "Finite_Set": various folding_XXX locales facilitate the
application of the various fold combinators on finite sets.
* Library theory "RBT" renamed to "RBT_Impl"; new library theory "RBT"
@@ -222,6 +222,9 @@
* Theory "Rational" renamed to "Rat", for consistency with "Nat",
"Int" etc. INCOMPATIBILITY.
+* Constant Rat.normalize needs to be qualified. Minor
+INCOMPATIBILITY.
+
* New set of rules "ac_simps" provides combined assoc / commute
rewrites for all interpretations of the appropriate generic locales.
@@ -493,13 +496,28 @@
*** ML ***
-* Sorts.certify_sort and derived "cert" operations for types and terms
-no longer minimize sorts. Thus certification at the boundary of the
-inference kernel becomes invariant under addition of class relations,
-which is an important monotonicity principle. Sorts are now minimized
-in the syntax layer only, at the boundary between the end-user and the
-system. Subtle INCOMPATIBILITY, may have to use Sign.minimize_sort
-explicitly in rare situations.
+* Renamed some important ML structures, while keeping the old names
+for some time as aliases within the structure Legacy:
+
+ OuterKeyword ~> Keyword
+ OuterLex ~> Token
+ OuterParse ~> Parse
+ OuterSyntax ~> Outer_Syntax
+ SpecParse ~> Parse_Spec
+
+Note that "open Legacy" simplifies porting of sources, but forgetting
+to remove it again will complicate porting again in the future.
+
+* Most operations that refer to a global context are named
+accordingly, e.g. Simplifier.global_context or
+ProofContext.init_global. There are some situations where a global
+context actually works, but under normal circumstances one needs to
+pass the proper local context through the code!
+
+* Discontinued old TheoryDataFun with its copy/init operation -- data
+needs to be pure. Functor Theory_Data_PP retains the traditional
+Pretty.pp argument to merge, which is absent in the standard
+Theory_Data version.
* Antiquotations for basic formal entities:
@@ -522,21 +540,21 @@
values similar to the ML toplevel. The result is compiler dependent
and may fall back on "?" in certain situations.
+* Sorts.certify_sort and derived "cert" operations for types and terms
+no longer minimize sorts. Thus certification at the boundary of the
+inference kernel becomes invariant under addition of class relations,
+which is an important monotonicity principle. Sorts are now minimized
+in the syntax layer only, at the boundary between the end-user and the
+system. Subtle INCOMPATIBILITY, may have to use Sign.minimize_sort
+explicitly in rare situations.
+
* Renamed old-style Drule.standard to Drule.export_without_context, to
emphasize that this is in no way a standard operation.
INCOMPATIBILITY.
-* Curried take and drop in library.ML; negative length is interpreted
-as infinity (as in chop). INCOMPATIBILITY.
-
* Subgoal.FOCUS (and variants): resulting goal state is normalized as
usual for resolution. Rare INCOMPATIBILITY.
-* Discontinued old TheoryDataFun with its copy/init operation -- data
-needs to be pure. Functor Theory_Data_PP retains the traditional
-Pretty.pp argument to merge, which is absent in the standard
-Theory_Data version.
-
* Renamed varify/unvarify operations to varify_global/unvarify_global
to emphasize that these only work in a global situation (which is
quite rare).
@@ -544,23 +562,11 @@
* Configuration options now admit dynamic default values, depending on
the context or even global references.
-* Most operations that refer to a global context are named
-accordingly, e.g. Simplifier.global_context or
-ProofContext.init_global. There are some situations where a global
-context actually works, but under normal circumstances one needs to
-pass the proper local context through the code!
-
-* Renamed some important ML structures, while keeping the old names
-for some time as aliases within the structure Legacy:
-
- OuterKeyword ~> Keyword
- OuterLex ~> Token
- OuterParse ~> Parse
- OuterSyntax ~> Outer_Syntax
- SpecParse ~> Parse_Spec
-
-Note that "open Legacy" simplifies porting of sources, but forgetting
-to remove it again will complicate porting again in the future.
+* SHA1.digest digests strings according to SHA-1 (see RFC 3174). It
+uses an efficient external library if available (for Poly/ML).
+
+* Curried take and drop in library.ML; negative length is interpreted
+as infinity (as in chop). Subtle INCOMPATIBILITY.
*** System ***
--- a/src/HOL/Rat.thy Thu May 27 16:29:33 2010 +0200
+++ b/src/HOL/Rat.thy Thu May 27 16:30:26 2010 +0200
@@ -1203,4 +1203,7 @@
lemma "123.456 = -111.111 + 200 + 30 + 4 + 5/10 + 6/100 + (7/1000::rat)"
by simp
+
+hide_const (open) normalize
+
end