--- a/NEWS Wed Feb 22 16:21:26 2017 +0000
+++ b/NEWS Wed Feb 22 20:24:50 2017 +0100
@@ -12,6 +12,17 @@
* 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: …} : ('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.
+
*** Prover IDE -- Isabelle/Scala/jEdit ***