
diff -r 1d6926f96440 -r 12741f23527d src/HOL/ex/Predicate_Compile_ex.thy
--- 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




