--- a/CONTRIBUTORS Sun Apr 01 22:41:56 2012 +0200
+++ b/CONTRIBUTORS Sun Apr 01 22:55:06 2012 +0200
@@ -6,9 +6,13 @@
Contributions to this Isabelle version
--------------------------------------
-* January 2011: Florian Haftmann, TUM, et. al.
+* January 2012: Florian Haftmann, TUM, et. al.
(Re-)Introduction of the "set" type constructor.
+* March 2012: Cezary Kaliszyk, University of Innsbruck and
+ Alexander Krauss, QAware GmbH
+ Faster and more scalable Import mechanism for HOL Light proofs.
+
Contributions to Isabelle2011-1
-------------------------------
--- a/NEWS Sun Apr 01 22:41:56 2012 +0200
+++ b/NEWS Sun Apr 01 22:55:06 2012 +0200
@@ -135,9 +135,10 @@
* Code generation by default implements sets as container type rather
than predicates. INCOMPATIBILITY.
-* New proof import from HOL Light, cf. HOL/Import. Requires a proof
-bundle, which is available as an external component. Removed old (and
-mostly dead) Importer for HOL4 and HOL Light. INCOMPATIBILITY.
+* New proof import from HOL Light: Faster, simpler, and more scalable.
+Requires a proof bundle, which is available as an external component.
+Removed old (and mostly dead) Importer for HOL4 and HOL Light.
+INCOMPATIBILITY.
* New type synonym 'a rel = ('a * 'a) set