--- a/doc-src/TutorialI/CodeGen/CodeGen.thy Wed Sep 21 13:28:44 2005 +0200
+++ b/doc-src/TutorialI/CodeGen/CodeGen.thy Wed Sep 21 14:00:28 2005 +0200
@@ -28,7 +28,7 @@
values is easily defined:
*}
-consts value :: "('a,'v)expr \<Rightarrow> ('a \<Rightarrow> 'v) \<Rightarrow> 'v";
+consts "value" :: "('a,'v)expr \<Rightarrow> ('a \<Rightarrow> 'v) \<Rightarrow> 'v";
primrec
"value (Cex v) env = v"
"value (Vex a) env = env a"
--- a/doc-src/TutorialI/Ifexpr/Ifexpr.thy Wed Sep 21 13:28:44 2005 +0200
+++ b/doc-src/TutorialI/Ifexpr/Ifexpr.thy Wed Sep 21 14:00:28 2005 +0200
@@ -36,7 +36,7 @@
values:
*}
-consts value :: "boolex \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool";
+consts "value" :: "boolex \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool";
primrec
"value (Const b) env = b"
"value (Var x) env = env x"
--- a/doc-src/TutorialI/Trie/Trie.thy Wed Sep 21 13:28:44 2005 +0200
+++ b/doc-src/TutorialI/Trie/Trie.thy Wed Sep 21 14:00:28 2005 +0200
@@ -19,7 +19,7 @@
We define two selector functions:
*};
-consts value :: "('a,'v)trie \<Rightarrow> 'v option"
+consts "value" :: "('a,'v)trie \<Rightarrow> 'v option"
alist :: "('a,'v)trie \<Rightarrow> ('a * ('a,'v)trie)list";
primrec "value(Trie ov al) = ov";
primrec "alist(Trie ov al) = al";