Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Metis_Examples/Message.thy
changeset 36580 d23a3a4d1849
parent 36553 95bdfa572cee
child 36911 0e2818493775 
--- 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))"
isabelle