--- 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
@@ -70,12 +70,12 @@
qed
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)"