--- a/src/HOL/ex/Predicate_Compile_ex.thy Sun Jun 28 22:51:29 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile_ex.thy Mon Jun 29 12:33:58 2009 +0200
@@ -58,11 +58,11 @@
lemma [code_pred_intros]:
"r a b ==> tranclp r a b"
-"r a b ==> tranclp r b c ==> tranclp r a c"
+"r a b ==> tranclp r b c ==> tranclp r a c"
by auto
(* Setup requires quick and dirty proof *)
-(*
+
code_pred tranclp
proof -
case tranclp
@@ -70,7 +70,6 @@
qed
thm tranclp.equation
-*)
inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
"succ 0 1"