# HG changeset patch
# User wenzelm
# Date 1272644944 -7200
# Node ID d23a3a4d1849a42ca52c0407f181b283ca5a21f1
# Parent  04dd306fdb3cc748eac8dac47ad16ec222480bb2
eliminated spurious sledgehammer invocation;

diff -r 04dd306fdb3c -r d23a3a4d1849 src/HOL/Metis_Examples/Message.thy
--- a/src/HOL/Metis_Examples/Message.thy	Fri Apr 30 18:12:41 2010 +0200
+++ b/src/HOL/Metis_Examples/Message.thy	Fri Apr 30 18:29:04 2010 +0200
@@ -711,7 +711,7 @@
 lemma Fake_parts_insert:
      "X \<in> synth (analz H) ==>  
       parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
-sledgehammer
+(*sledgehammer*)
 proof -
   assume A1: "X \<in> synth (analz H)"
   have F1: "\<forall>x\<^isub>1. analz x\<^isub>1 \<union> synth (analz x\<^isub>1) = analz (synth (analz x\<^isub>1))"