NEWS and CONTRIBUTORS
authorhaftmann
Tue Aug 17 14:33:39 2010 +0200 (2010-08-17)
changeset 3846175fc4087764e
parent 38460 628fee3eb449
child 38462 34d3de1254cd
NEWS and CONTRIBUTORS
CONTRIBUTORS
NEWS
     1.1 --- a/CONTRIBUTORS	Tue Aug 17 14:19:12 2010 +0200
     1.2 +++ b/CONTRIBUTORS	Tue Aug 17 14:33:39 2010 +0200
     1.3 @@ -6,6 +6,9 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 +* July 2010: Florian Haftmann, TUM
     1.8 +  Reworking and extension of the Isabelle/HOL framework.
     1.9 +
    1.10  
    1.11  Contributions to Isabelle2009-2
    1.12  --------------------------------------
     2.1 --- a/NEWS	Tue Aug 17 14:19:12 2010 +0200
     2.2 +++ b/NEWS	Tue Aug 17 14:33:39 2010 +0200
     2.3 @@ -35,11 +35,17 @@
     2.4  
     2.5  *** HOL ***
     2.6  
     2.7 +* Session Imperative_HOL: revamped, corrected dozens of inadequacies.
     2.8 +INCOMPATIBILITY.
     2.9 +
    2.10 +* Quickcheck in locales considers interpretations of that locale for
    2.11 +counter example search.
    2.12 +
    2.13  * Theory Library/Monad_Syntax provides do-syntax for monad types.  Syntax
    2.14  in Library/State_Monad has been changed to avoid ambiguities.
    2.15  INCOMPATIBILITY.
    2.16  
    2.17 -* code generator: export_code without explicit file declaration prints
    2.18 +* Code generator: export_code without explicit file declaration prints
    2.19  to standard output.  INCOMPATIBILITY.
    2.20  
    2.21  * Abolished symbol type names:  "prod" and "sum" replace "*" and "+"
    2.22 @@ -121,8 +127,8 @@
    2.23  INCOMPATIBILITY.
    2.24  
    2.25  * Inductive package: offers new command "inductive_simps" to automatically
    2.26 -  derive instantiated and simplified equations for inductive predicates,
    2.27 -  similar to inductive_cases.
    2.28 +derive instantiated and simplified equations for inductive predicates,
    2.29 +similar to inductive_cases.
    2.30  
    2.31  
    2.32  *** ML ***