--- a/NEWS Wed Feb 22 21:12:23 2017 +0100
+++ b/NEWS Fri Feb 24 12:24:13 2017 +0100
@@ -16,9 +16,9 @@
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
+ @{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