# HG changeset patch
# User wenzelm
# Date 1430770295 -7200
# Node ID e0c3e11e9bea53656fdd1a258ac66c2e74390582
# Parent  2795bd5e502ed0601759332e68389f3995b40130
tuned;

diff -r 2795bd5e502e -r e0c3e11e9bea CONTRIBUTORS
--- a/CONTRIBUTORS	Mon May 04 16:12:37 2015 +0200
+++ b/CONTRIBUTORS	Mon May 04 22:11:35 2015 +0200
@@ -10,8 +10,8 @@
   The Eisbach proof method language and "match" method.
 
 * Winter 2014 and Spring 2015: Ondrej Kuncar, TUM
-  Extension of lift_definition to execute lifted functions that have as a return type 
-  a datatype containing a subtype. 
+  Extension of lift_definition to execute lifted functions that have as a
+  return type a datatype containing a subtype.
 
 * March 2015: Jasmin Blanchette, Inria & LORIA & MPII, Mathias Fleury, MPII,
   and Dmitriy Traytel, TUM
diff -r 2795bd5e502e -r e0c3e11e9bea NEWS
--- a/NEWS	Mon May 04 16:12:37 2015 +0200
+++ b/NEWS	Mon May 04 22:11:35 2015 +0200
@@ -216,11 +216,10 @@
     of rel_prod_def and rel_sum_def.
     Minor INCOMPATIBILITY: (rarely used by name) transfer theorem names
     changed (e.g. map_prod_transfer ~> prod.map_transfer).
-  - Parametricity theorems for map functions, relators, set
-    functions, constructors, case combinators, discriminators,
-    selectors and (co)recursors are automatically proved and registred
-    as transfer rules.
-
+  - Parametricity theorems for map functions, relators, set functions,
+    constructors, case combinators, discriminators, selectors and
+    (co)recursors are automatically proved and registered as transfer
+    rules.
 
 * Old datatype package:
   - The old 'datatype' command has been renamed 'old_datatype', and
@@ -266,12 +265,10 @@
   - New option 'smt_statistics' to display statistics of the new 'smt'
     method, especially runtime statistics of Z3 proof reconstruction.
 
-* Lifting
-  - lift_definition command implements a workaround that allows us 
-    to execute lifted constants that have as a return type 
-    a datatype containing a subtype.
-    This was a long time limitation in the area of code generation and
-    lifting and the used workarounds were tedious.
+* Lifting: command 'lift_definition' allows to execute lifted constants
+that have as a return type a datatype containing a subtype. This
+overcomes long-time limitations in the area of code generation and
+lifting, and avoids tedious workarounds.
 
 * Command and antiquotation "value" provide different evaluation slots
 (again), where the previous strategy (NBE after ML) serves as default.