diff -r dd5a31098f85 -r 0e2818493775 src/HOL/Metis_Examples/Message.thy
--- a/src/HOL/Metis_Examples/Message.thy	Fri May 14 11:24:14 2010 +0200
+++ b/src/HOL/Metis_Examples/Message.thy	Fri May 14 11:24:49 2010 +0200
@@ -9,7 +9,7 @@
 begin
 
 lemma strange_Un_eq [simp]: "A \<union> (B \<union> A) = B \<union> A"
-by (metis Un_ac(2) Un_ac(3))
+by (metis Un_commute Un_left_absorb)
 
 types 
   key = nat
@@ -681,14 +681,10 @@
 
 lemma analz_synth [simp]: "analz (synth H) = analz H \<union> synth H"
 proof -
-  have "\<forall>x\<^isub>2 x\<^isub>1. synth x\<^isub>1 \<union> analz (x\<^isub>1 \<union> x\<^isub>2) = analz (synth x\<^isub>1 \<union> x\<^isub>2)"
-    by (metis Un_commute analz_synth_Un)
-  hence "\<forall>x\<^isub>3 x\<^isub>1. synth x\<^isub>1 \<union> analz x\<^isub>1 = analz (synth x\<^isub>1 \<union> UNION {} x\<^isub>3)"
-    by (metis UN_extend_simps(3))
-  hence "\<forall>x\<^isub>1. synth x\<^isub>1 \<union> analz x\<^isub>1 = analz (synth x\<^isub>1)"
-    by (metis UN_extend_simps(3))
-  hence "\<forall>x\<^isub>1. analz x\<^isub>1 \<union> synth x\<^isub>1 = analz (synth x\<^isub>1)"
-    by (metis Un_commute)
+  have "\<forall>x\<^isub>2 x\<^isub>1. synth x\<^isub>1 \<union> analz (x\<^isub>1 \<union> x\<^isub>2) = analz (synth x\<^isub>1 \<union> x\<^isub>2)" by (metis Un_commute analz_synth_Un)
+  hence "\<forall>x\<^isub>1. synth x\<^isub>1 \<union> analz x\<^isub>1 = analz (synth x\<^isub>1 \<union> {})" by (metis Un_empty_right)
+  hence "\<forall>x\<^isub>1. synth x\<^isub>1 \<union> analz x\<^isub>1 = analz (synth x\<^isub>1)" by (metis Un_empty_right)
+  hence "\<forall>x\<^isub>1. analz x\<^isub>1 \<union> synth x\<^isub>1 = analz (synth x\<^isub>1)" by (metis Un_commute)
   thus "analz (synth H) = analz H \<union> synth H" by metis
 qed
 
@@ -698,20 +694,18 @@
 lemma parts_insert_subset_Un: "X\<in> G ==> parts(insert X H) \<subseteq> parts G \<union> parts H"
 proof -
   assume "X \<in> G"
-  hence "\<forall>u. X \<in> G \<union> u" by (metis Un_iff)
-  hence "X \<in> G \<union> H \<and> H \<subseteq> G \<union> H"
-    by (metis Un_upper2)
-  hence "insert X H \<subseteq> G \<union> H" by (metis insert_subset)
-  hence "parts (insert X H) \<subseteq> parts (G \<union> H)"
-    by (metis parts_mono)
-  thus "parts (insert X H) \<subseteq> parts G \<union> parts H"
-    by (metis parts_Un)
+  hence "G X" by (metis mem_def)
+  hence "\<forall>x\<^isub>1. G \<subseteq> x\<^isub>1 \<longrightarrow> x\<^isub>1 X" by (metis predicate1D)
+  hence "\<forall>x\<^isub>1. (G \<union> x\<^isub>1) X" by (metis Un_upper1)
+  hence "\<forall>x\<^isub>1. X \<in> G \<union> x\<^isub>1" by (metis mem_def)
+  hence "insert X H \<subseteq> G \<union> H" by (metis Un_upper2 insert_subset)
+  hence "parts (insert X H) \<subseteq> parts (G \<union> H)" by (metis parts_mono)
+  thus "parts (insert X H) \<subseteq> parts G \<union> parts H" by (metis parts_Un)
 qed
 
 lemma Fake_parts_insert:
      "X \<in> synth (analz H) ==>  
       parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
-(*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))"