changeset 32665 | 8bf46a97ff79 |
parent 32579 | 73ad5dbf1034 |
child 32668 | b2de45007537 |
--- a/src/HOL/ex/Predicate_Compile_ex.thy Wed Sep 23 16:20:12 2009 +0200 +++ b/src/HOL/ex/Predicate_Compile_ex.thy Wed Sep 23 16:20:12 2009 +0200 @@ -44,7 +44,7 @@ "partition f [] [] []" | "f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) (x # ys) zs" | "\<not> f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) ys (x # zs)" - +ML {* set Toplevel.debug *} code_pred partition . thm partition.equation