NEWS
changeset 65042 956ea00a162a
parent 65041 2525e680f94f
child 65045 b69ef432438d
     1.1 --- a/NEWS	Wed Feb 22 20:24:50 2017 +0100
     1.2 +++ b/NEWS	Wed Feb 22 20:33:53 2017 +0100
     1.3 @@ -17,11 +17,12 @@
     1.4  the following antiquotations:
     1.5  
     1.6    @{computation … terms: … datatypes: …} : ((term -> term) -> 'ml option -> 'a) -> Proof.context -> term -> 'a
     1.7 -  @{computation_conv … terms: … datatypes: …} : ('ml -> conv) -> Proof.context -> conv
     1.8 +  @{computation_conv … terms: … datatypes: …} : (Proof.context -> 'ml -> conv) -> Proof.context -> conv
     1.9    @{computation_check terms: … datatypes: …} : Proof.context -> conv
    1.10  
    1.11  See src/HOL/ex/Computations.thy, src/HOL/Decision_Procs/Commutative_Ring.thy
    1.12 -and src/HOL/Decision_Procs/Reflective_Field.thy for examples.
    1.13 +and src/HOL/Decision_Procs/Reflective_Field.thy for examples and
    1.14 +the tutorial on code generation.
    1.15  
    1.16  
    1.17  *** Prover IDE -- Isabelle/Scala/jEdit ***