src/HOL/ex/Predicate_Compile_ex.thy

--- a/src/HOL/ex/Predicate_Compile_ex.thy	Thu Jun 11 21:39:08 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile_ex.thy	Thu Jun 11 22:04:23 2009 +0200
@@ -74,6 +74,8 @@
   show P by iprover
 qed  
 
+(* Setup requires quick and dirty proof *)
+(*
 code_pred tranclp
 proof -
   assume tranclp: "tranclp r a1 a2"
@@ -90,6 +92,7 @@
 qed
 
 thm tranclp.equation
+*)
 
 inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
     "succ 0 1"