less modest NEWS; CONTRIBUTORS
authorkrauss
Sun Apr 01 22:55:06 2012 +0200 (2012-04-01)
changeset 47265b8c98d476805
parent 47264 6488c5efec49
child 47266 bf9796e44584
less modest NEWS; CONTRIBUTORS
CONTRIBUTORS
NEWS
     1.1 --- a/CONTRIBUTORS	Sun Apr 01 22:41:56 2012 +0200
     1.2 +++ b/CONTRIBUTORS	Sun Apr 01 22:55:06 2012 +0200
     1.3 @@ -6,9 +6,13 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 -* January 2011: Florian Haftmann, TUM, et. al.
     1.8 +* January 2012: Florian Haftmann, TUM, et. al.
     1.9    (Re-)Introduction of the "set" type constructor.
    1.10  
    1.11 +* March 2012: Cezary Kaliszyk, University of Innsbruck and
    1.12 +  Alexander Krauss, QAware GmbH
    1.13 +  Faster and more scalable Import mechanism for HOL Light proofs.
    1.14 +
    1.15  
    1.16  Contributions to Isabelle2011-1
    1.17  -------------------------------
     2.1 --- a/NEWS	Sun Apr 01 22:41:56 2012 +0200
     2.2 +++ b/NEWS	Sun Apr 01 22:55:06 2012 +0200
     2.3 @@ -135,9 +135,10 @@
     2.4  * Code generation by default implements sets as container type rather
     2.5  than predicates.  INCOMPATIBILITY.
     2.6  
     2.7 -* New proof import from HOL Light, cf. HOL/Import. Requires a proof
     2.8 -bundle, which is available as an external component. Removed old (and
     2.9 -mostly dead) Importer for HOL4 and HOL Light.  INCOMPATIBILITY.
    2.10 +* New proof import from HOL Light: Faster, simpler, and more scalable.
    2.11 +Requires a proof bundle, which is available as an external component.
    2.12 +Removed old (and mostly dead) Importer for HOL4 and HOL Light.
    2.13 +INCOMPATIBILITY.
    2.14  
    2.15  * New type synonym 'a rel = ('a * 'a) set
    2.16