--- a/CONTRIBUTORS Thu Sep 23 08:30:33 2010 +0200
+++ b/CONTRIBUTORS Thu Sep 23 09:53:52 2010 +0200
@@ -6,11 +6,14 @@
Contributions to this Isabelle version
--------------------------------------
+* September 2010: Florian Haftmann, TUM
+ Code generation for Scala.
+
* August 2010: Johannes Hoelzl, Armin Heller, and Robert Himmelmann, TUM
Rewriting the Probability theory.
* July 2010: Florian Haftmann, TUM
- Reworking and extension of the Isabelle/HOL framework.
+ Reworking and extension of the Imperative HOL framework.
Contributions to Isabelle2009-2
@@ -86,7 +89,7 @@
New quickcheck implementation using new code generator.
* July 2009: Florian Haftmann, TUM
- HOL/Library/FSet: an explicit type of sets; finite sets ready to use
+ HOL/Library/Fset: an explicit type of sets; finite sets ready to use
for code generation.
* June 2009: Florian Haftmann, TUM
--- a/NEWS Thu Sep 23 08:30:33 2010 +0200
+++ b/NEWS Thu Sep 23 09:53:52 2010 +0200
@@ -74,12 +74,16 @@
*** HOL ***
+* Improved infrastructure for term evaluation using code generator
+techniques, in particular static evaluation conversions.
+
* String.literal is a type, but not a datatype. INCOMPATIBILITY.
* Renamed lemmas:
expand_fun_eq -> fun_eq_iff
expand_set_eq -> set_eq_iff
set_ext -> set_eqI
+ INCOMPATIBILITY.
* Renamed class eq and constant eq (for code generation) to class equal
and constant equal, plus renaming of related facts and various tuning.