NEWS
changeset 65041 2525e680f94f
parent 65027 2b8583507891
child 65042 956ea00a162a
     1.1 --- a/NEWS	Wed Feb 22 16:21:26 2017 +0000
     1.2 +++ b/NEWS	Wed Feb 22 20:24:50 2017 +0100
     1.3 @@ -12,6 +12,17 @@
     1.4  * Document antiquotations @{prf} and @{full_prf} output proof terms
     1.5  (again) in the same way as commands 'prf' and 'full_prf'.
     1.6  
     1.7 +* Computations generated by the code generator can be embedded
     1.8 +directly into ML, alongside with @{code} antiquotations, using
     1.9 +the following antiquotations:
    1.10 +
    1.11 +  @{computation … terms: … datatypes: …} : ((term -> term) -> 'ml option -> 'a) -> Proof.context -> term -> 'a
    1.12 +  @{computation_conv … terms: … datatypes: …} : ('ml -> conv) -> Proof.context -> conv
    1.13 +  @{computation_check terms: … datatypes: …} : Proof.context -> conv
    1.14 +
    1.15 +See src/HOL/ex/Computations.thy, src/HOL/Decision_Procs/Commutative_Ring.thy
    1.16 +and src/HOL/Decision_Procs/Reflective_Field.thy for examples.
    1.17 +
    1.18  
    1.19  *** Prover IDE -- Isabelle/Scala/jEdit ***
    1.20