
diff -r 67f0cb151eb2 -r 16a2ed09217a doc-src/Codegen/Thy/Inductive_Predicate.thy
--- a/doc-src/Codegen/Thy/Inductive_Predicate.thy	Thu Sep 02 16:41:42 2010 +0200
+++ b/doc-src/Codegen/Thy/Inductive_Predicate.thy	Thu Sep 02 16:41:42 2010 +0200
@@ -220,8 +220,8 @@
   "values"} and the number of elements.
 *}
 
-values %quote [mode: i \<Rightarrow> o \<Rightarrow> bool] 20 "{n. tranclp succ 10 n}"
-values %quote [mode: o \<Rightarrow> i \<Rightarrow> bool] 10 "{n. tranclp succ n 10}"
+values %quote [mode: i \<Rightarrow> o \<Rightarrow> bool] 1 "{n. tranclp succ 10 n}" (*FIMXE does not terminate for n\<ge>1*)
+values %quote [mode: o \<Rightarrow> i \<Rightarrow> bool] 1 "{n. tranclp succ n 10}"
 
 
 subsection {* Embedding into functional code within Isabelle/HOL *}




