src/HOL/ex/Predicate_Compile_ex.thy

--- 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
@@ -62,7 +62,7 @@
 by auto
 
 (* Setup requires quick and dirty proof *)
-(*
+
 code_pred tranclp
 proof -
   case tranclp
@@ -70,7 +70,7 @@
 qed
 
 thm tranclp.equation
-*)
+
 inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
     "succ 0 1"
   | "succ m n \<Longrightarrow> succ (Suc m) (Suc n)"