--- a/src/HOL/ex/Predicate_Compile_ex.thy Mon May 18 15:45:38 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile_ex.thy Mon May 18 15:45:42 2009 +0200
@@ -12,6 +12,8 @@
thm even.equation
+ML_val {* Predicate.yieldn 10 @{code even_0} *}
+
inductive append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
append_Nil: "append [] xs xs"
@@ -22,6 +24,8 @@
thm append.equation
+ML_val {* Predicate.yieldn 10 (@{code append_3} [1, 2, 3]) *}
+
inductive partition :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
for f where