diff -r a3357a631b96 -r 2478dd225b68 src/HOL/Metis_Examples/TransClosure.thy
--- a/src/HOL/Metis_Examples/TransClosure.thy	Wed Apr 28 16:03:49 2010 +0200
+++ b/src/HOL/Metis_Examples/TransClosure.thy	Wed Apr 28 16:05:38 2010 +0200
@@ -5,7 +5,7 @@
 *)
 
 theory TransClosure
-imports Sledgehammer2d (* ### *)
+imports Main
 begin
 
 types addr = nat
@@ -23,7 +23,19 @@
 
 lemma "\<lbrakk>f c = Intg x; \<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x; (a, b) \<in> R\<^sup>*; (b, c) \<in> R\<^sup>*\<rbrakk>
        \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
-by (metis converse_rtranclE transitive_closure_trans(6))
+sledgehammer
+proof -
+  assume A1: "f c = Intg x"
+  assume A2: "\<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x"
+  assume A3: "(a, b) \<in> R\<^sup>*"
+  assume A4: "(b, c) \<in> R\<^sup>*"
+  have F1: "f c \<noteq> f b" using A2 A1 by metis
+  have F2: "\<forall>u. (b, u) \<in> R \<longrightarrow> (a, u) \<in> R\<^sup>*" using A3 by (metis transitive_closure_trans(6))
+  have F3: "\<exists>x. (b, x R b c) \<in> R \<or> c = b" using A4 by (metis converse_rtranclE)
+  have "c \<noteq> b" using F1 by metis
+  hence "\<exists>u. (b, u) \<in> R" using F3 by metis
+  thus "\<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*" using F2 by metis
+qed
 
 lemma "\<lbrakk>f c = Intg x; \<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x; (a, b) \<in> R\<^sup>*; (b,c) \<in> R\<^sup>*\<rbrakk>
        \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
@@ -36,7 +48,7 @@
   have "(R\<^sup>*) (a, b)" using A3 by (metis mem_def)
   hence F1: "(a, b) \<in> R\<^sup>*" by (metis mem_def)
   have "b \<noteq> c" using A1 A2 by metis
-  hence "\<exists>x\<^isub>1. (b, x\<^isub>1) \<in> R" using A4 by (metis mem_def converse_rtranclE)
+  hence "\<exists>x\<^isub>1. (b, x\<^isub>1) \<in> R" using A4 by (metis converse_rtranclE)
   thus "\<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*" using F1 by (metis transitive_closure_trans(6))
 qed