# HG changeset patch
# User wenzelm
# Date 1272476625 -7200
# Node ID 6c7ba330ab42bf28857570273b23198af903d696
# Parent  620f899158d421e25a3016ed75b281732902b85b
disabled spurious invocation of (interactive) sledgehammer;

diff -r 620f899158d4 -r 6c7ba330ab42 src/HOL/Metis_Examples/TransClosure.thy
--- a/src/HOL/Metis_Examples/TransClosure.thy	Wed Apr 28 17:29:58 2010 +0200
+++ b/src/HOL/Metis_Examples/TransClosure.thy	Wed Apr 28 19:43:45 2010 +0200
@@ -23,7 +23,7 @@
 
 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>*"
-sledgehammer
+(* sledgehammer *)
 proof -
   assume A1: "f c = Intg x"
   assume A2: "\<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x"