# HG changeset patch
# User haftmann
# Date 1242654342 -7200
# Node ID 12741f23527dfb43e2a8d37d0dd03431489165d2
# Parent  1d6926f96440cf8303110640ffb6486c7c454f20
added example on ML level

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