# HG changeset patch
# User wenzelm
# Date 1127304028 -7200
# Node ID 23c4a349feffd8da43b40d27c0e582894c38fd0f
# Parent  d16abc8f4fb059d1490a840479bf154e76cff703
quote "value";

diff -r d16abc8f4fb0 -r 23c4a349feff doc-src/TutorialI/CodeGen/CodeGen.thy
--- 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"
diff -r d16abc8f4fb0 -r 23c4a349feff doc-src/TutorialI/Ifexpr/Ifexpr.thy
--- 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"
diff -r d16abc8f4fb0 -r 23c4a349feff doc-src/TutorialI/Trie/Trie.thy
--- 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";