| changeset 17555 | 23c4a349feff |
| parent 17212 | 6859484b5b2b |
| child 27015 | f8537d69f514 |
--- 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"