# HG changeset patch # User haftmann # Date 1283438502 -7200 # Node ID 16a2ed09217a1090013880256c9ceb778b963ada # Parent 67f0cb151eb284c743646e43fe1fa9dcc7630f57 set depth to 1 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 \ o \ bool] 20 "{n. tranclp succ 10 n}" -values %quote [mode: o \ i \ bool] 10 "{n. tranclp succ n 10}" +values %quote [mode: i \ o \ bool] 1 "{n. tranclp succ 10 n}" (*FIMXE does not terminate for n\1*) +values %quote [mode: o \ i \ bool] 1 "{n. tranclp succ n 10}" subsection {* Embedding into functional code within Isabelle/HOL *}