--- 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 ***