more precise NEWS and CONTRIBUTORS
authorhaftmann
Wed Feb 22 20:33:53 2017 +0100 (2017-02-22)
changeset 65042956ea00a162a
parent 65041 2525e680f94f
child 65043 fd753468786f
more precise NEWS and CONTRIBUTORS
CONTRIBUTORS
NEWS
     1.1 --- a/CONTRIBUTORS	Wed Feb 22 20:24:50 2017 +0100
     1.2 +++ b/CONTRIBUTORS	Wed Feb 22 20:33:53 2017 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  --------------------------------------
     1.5  
     1.6  * February 2017: Florian Haftmann, TUM
     1.7 -  Statically embedded computatations implementated by generated code.
     1.8 +  Statically embedded computations implemented by generated code.
     1.9  
    1.10  
    1.11  Contributions to Isabelle2016-1
     2.1 --- a/NEWS	Wed Feb 22 20:24:50 2017 +0100
     2.2 +++ b/NEWS	Wed Feb 22 20:33:53 2017 +0100
     2.3 @@ -17,11 +17,12 @@
     2.4  the following antiquotations:
     2.5  
     2.6    @{computation … terms: … datatypes: …} : ((term -> term) -> 'ml option -> 'a) -> Proof.context -> term -> 'a
     2.7 -  @{computation_conv … terms: … datatypes: …} : ('ml -> conv) -> Proof.context -> conv
     2.8 +  @{computation_conv … terms: … datatypes: …} : (Proof.context -> 'ml -> conv) -> Proof.context -> conv
     2.9    @{computation_check terms: … datatypes: …} : Proof.context -> conv
    2.10  
    2.11  See src/HOL/ex/Computations.thy, src/HOL/Decision_Procs/Commutative_Ring.thy
    2.12 -and src/HOL/Decision_Procs/Reflective_Field.thy for examples.
    2.13 +and src/HOL/Decision_Procs/Reflective_Field.thy for examples and
    2.14 +the tutorial on code generation.
    2.15  
    2.16  
    2.17  *** Prover IDE -- Isabelle/Scala/jEdit ***