# HG changeset patch
# User haftmann
# Date 1487792033 -3600
# Node ID 956ea00a162aea5308c66829c84d360a00fe32dc
# Parent  2525e680f94ff4362d05ab6107ded1e975104585
more precise NEWS and CONTRIBUTORS

diff -r 2525e680f94f -r 956ea00a162a CONTRIBUTORS
--- a/CONTRIBUTORS	Wed Feb 22 20:24:50 2017 +0100
+++ b/CONTRIBUTORS	Wed Feb 22 20:33:53 2017 +0100
@@ -7,7 +7,7 @@
 --------------------------------------
 
 * February 2017: Florian Haftmann, TUM
-  Statically embedded computatations implementated by generated code.
+  Statically embedded computations implemented by generated code.
 
 
 Contributions to Isabelle2016-1
diff -r 2525e680f94f -r 956ea00a162a NEWS
--- a/NEWS	Wed Feb 22 20:24:50 2017 +0100
+++ b/NEWS	Wed Feb 22 20:33:53 2017 +0100
@@ -17,11 +17,12 @@
 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_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 src/HOL/Decision_Procs/Reflective_Field.thy for examples and
+the tutorial on code generation.
 
 
 *** Prover IDE -- Isabelle/Scala/jEdit ***