--- a/CONTRIBUTORS Fri Jan 08 15:49:01 2016 +0100
+++ b/CONTRIBUTORS Fri Jan 08 15:54:43 2016 +0100
@@ -1,7 +1,7 @@
For the purposes of the license agreement in the file COPYRIGHT, a
-'contributor' is anybody who is listed in this file (CONTRIBUTORS) or
-who is listed as an author in one of the source files of this Isabelle
-distribution.
+'contributor' is anybody who is listed in this file (CONTRIBUTORS) or who is
+listed as an author in one of the source files of this Isabelle distribution.
+
Contributions to Isabelle2016
-----------------------------
@@ -696,3 +696,5 @@
* 2004/2005: Tjark Weber, TUM
SAT solver method using zChaff.
Improved version of HOL/refute.
+
+:maxLineLen=78:
--- a/NEWS Fri Jan 08 15:49:01 2016 +0100
+++ b/NEWS Fri Jan 08 15:54:43 2016 +0100
@@ -568,10 +568,9 @@
being defined.
- Avoid various internal name clashes (e.g., 'datatype f = f').
-* Transfer:
- - new methods for interactive debugging of 'transfer' and
- 'transfer_prover': 'transfer_start', 'transfer_step', 'transfer_end',
- 'transfer_prover_start' and 'transfer_prover_end'.
+* Transfer: new methods for interactive debugging of 'transfer' and
+'transfer_prover': 'transfer_start', 'transfer_step', 'transfer_end',
+'transfer_prover_start' and 'transfer_prover_end'.
* Division on integers is bootstrapped directly from division on
naturals and uses generic numeral algorithm for computations. Slight
@@ -651,8 +650,9 @@
* Library/Periodic_Fun: a locale that provides convenient lemmas for
periodic functions.
-* Library/Formal_Power_Series: proper definition of division (with remainder)
-for formal power series; instances for Euclidean Ring and GCD.
+* Library/Formal_Power_Series: proper definition of division (with
+remainder) for formal power series; instances for Euclidean Ring and
+GCD.
* HOL-Imperative_HOL: obsolete theory Legacy_Mrec has been removed.