src/HOL/ex/Predicate_Compile_ex.thy

   case tranclp
   from this converse_tranclpE[OF this(1)] show thesis by metis
 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)"
 
 code_pred succ .