# HG changeset patch
# User wenzelm
# Date 1488149419 -3600
# Node ID 12189e86c49d20737a96e0372d267af8fb229459
# Parent  9ad3f65c03f4e5025bd1003d617e00f00cefe179
tuned whitespace;

diff -r 9ad3f65c03f4 -r 12189e86c49d NEWS
--- a/NEWS	Sun Feb 26 22:41:10 2017 +0100
+++ b/NEWS	Sun Feb 26 23:50:19 2017 +0100
@@ -12,17 +12,20 @@
 * Document antiquotations @{prf} and @{full_prf} output proof terms
 (again) in the same way as commands 'prf' and 'full_prf'.
 
-* Computations generated by the code generator can be embedded
-directly into ML, alongside with @{code} antiquotations, using
-the following antiquotations:
-
-  @{computation ... terms: ... datatypes: ...} : ((term -> term) -> 'ml option -> 'a) -> Proof.context -> term -> 'a
-  @{computation_conv ... terms: ... datatypes: ...} : (Proof.context -> 'ml -> conv) -> Proof.context -> conv
+* Computations generated by the code generator can be embedded directly
+into ML, alongside with @{code} antiquotations, using the following
+antiquotations:
+
+  @{computation ... terms: ... datatypes: ...} :
+    ((term -> term) -> 'ml option -> 'a) -> Proof.context -> term -> 'a
+  @{computation_conv ... terms: ... datatypes: ...} :
+    (Proof.context -> 'ml -> conv) -> Proof.context -> conv
   @{computation_check terms: ... datatypes: ...} : Proof.context -> conv
 
-See src/HOL/ex/Computations.thy, src/HOL/Decision_Procs/Commutative_Ring.thy
-and src/HOL/Decision_Procs/Reflective_Field.thy for examples and
-the tutorial on code generation.
+See src/HOL/ex/Computations.thy,
+src/HOL/Decision_Procs/Commutative_Ring.thy and
+src/HOL/Decision_Procs/Reflective_Field.thy for examples and the
+tutorial on code generation.
 
 
 *** Prover IDE -- Isabelle/Scala/jEdit ***
@@ -108,13 +111,14 @@
 * The theorem in Permutations has been renamed:
   bij_swap_ompose_bij ~> bij_swap_compose_bij
 
-* Session HOL-Library: The simprocs on subsets operators of multisets have been renamed:
+* Session HOL-Library: The simprocs on subsets operators of multisets
+have been renamed:
   msetless_cancel_numerals ~> msetsubset_cancel
   msetle_cancel_numerals ~> msetsubset_eq_cancel
 INCOMPATIBILITY.
 
-* Session HOL-Library: The suffix _numerals has been removed from the name of the simprocs on multisets.
-INCOMPATIBILITY.
+* Session HOL-Library: The suffix _numerals has been removed from the
+name of the simprocs on multisets. INCOMPATIBILITY.
 
 
 *** System ***