--- a/src/HOL/ex/Predicate_Compile_ex.thy Tue Aug 04 08:34:56 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile_ex.thy Tue Aug 04 08:34:56 2009 +0200
@@ -71,6 +71,11 @@
thm tranclp.equation
+setup {* Predicate_Compile.add_sizelim_equations [@{const_name tranclp}] *}
+setup {* fn thy => exception_trace (fn () => Predicate_Compile.add_quickcheck_equations [@{const_name tranclp}] thy) *}
+
+thm tranclp.rpred_equation
+
inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
"succ 0 1"
| "succ m n \<Longrightarrow> succ (Suc m) (Suc n)"