# HG changeset patch
# User wenzelm
# Date 1127755153 -7200
# Node ID a8b83a82c4c61e3f6265a17f78709dfb4a9c58ac
# Parent  0039abe8881665a035f1c5cd040c9f9340b4f8a7
quote 'value';

diff -r 0039abe88816 -r a8b83a82c4c6 doc-src/TutorialI/Overview/LNCS/FP1.thy
--- a/doc-src/TutorialI/Overview/LNCS/FP1.thy	Mon Sep 26 19:19:12 2005 +0200
+++ b/doc-src/TutorialI/Overview/LNCS/FP1.thy	Mon Sep 26 19:19:13 2005 +0200
@@ -154,7 +154,7 @@
                      | Vex 'a
                      | Bex "'v binop"  "('a,'v)expr"  "('a,'v)expr"
 
-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"