--- 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
--- 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 ***