# HG changeset patch
# User wenzelm
# Date 1312922253 -7200
# Node ID 60edd70b72bd35763880e54499554eb152df57ca
# Parent  0e018cbcc0de519b9422076e01c907ebe46b1f70# Parent  202d2f56560c71e38eb117424ec1010238f3c7a8
merged

diff -r 202d2f56560c -r 60edd70b72bd NEWS
--- a/NEWS	Tue Aug 09 22:30:33 2011 +0200
+++ b/NEWS	Tue Aug 09 22:37:33 2011 +0200
@@ -67,19 +67,27 @@
 generalized theorems INF_cong and SUP_cong.  New type classes for complete
 boolean algebras and complete linear orders.  Lemmas Inf_less_iff,
 less_Sup_iff, INF_less_iff, less_SUP_iff now reside in class complete_linorder.
-Changes proposition of lemmas Inf_fun_def, Sup_fun_def, Inf_apply, Sup_apply.
-Redundant lemmas Inf_singleton, Sup_singleton, Inf_binary and Sup_binary have
-been discarded.
+Changed proposition of lemmas Inf_fun_def, Sup_fun_def, Inf_apply, Sup_apply.
+Redundant lemmas Inf_singleton, Sup_singleton, Inf_binary, Sup_binary,
+INF_eq, SUP_eq, INF_UNIV_range, SUP_UNIV_range, Int_eq_Inter,
+INTER_eq_Inter_image, Inter_def, INT_eq, Un_eq_Union, UNION_eq_Union_image,
+Union_def, UN_singleton, UN_eq have been discarded.
 More consistent and less misunderstandable names:
   INFI_def ~> INF_def
   SUPR_def ~> SUP_def
-  le_SUPI ~> le_SUP_I
-  le_SUPI2 ~> le_SUP_I2
-  le_INFI ~> le_INF_I
+  INF_leI ~> INF_lower
+  INF_leI2 ~> INF_lower2
+  le_INFI ~> INF_greatest
+  le_SUPI ~> SUP_upper
+  le_SUPI2 ~> SUP_upper2
+  SUP_leI ~> SUP_least
   INFI_bool_eq ~> INF_bool_eq
   SUPR_bool_eq ~> SUP_bool_eq
   INFI_apply ~> INF_apply
   SUPR_apply ~> SUP_apply
+  INTER_def ~> INTER_eq
+  UNION_def ~> UNION_eq
+
 INCOMPATIBILITY.
 
 * Theorem collections ball_simps and bex_simps do not contain theorems referring
diff -r 202d2f56560c -r 60edd70b72bd src/HOL/Algebra/Ideal.thy
--- a/src/HOL/Algebra/Ideal.thy	Tue Aug 09 22:30:33 2011 +0200
+++ b/src/HOL/Algebra/Ideal.thy	Tue Aug 09 22:37:33 2011 +0200
@@ -227,26 +227,14 @@
     and notempty: "S \<noteq> {}"
   shows "ideal (Inter S) R"
 apply (unfold_locales)
-apply (simp_all add: Inter_def INTER_def)
-      apply (rule, simp) defer 1
+apply (simp_all add: Inter_eq)
+      apply rule unfolding mem_Collect_eq defer 1
       apply rule defer 1
       apply rule defer 1
       apply (fold a_inv_def, rule) defer 1
       apply rule defer 1
       apply rule defer 1
 proof -
-  fix x
-  assume "\<forall>I\<in>S. x \<in> I"
-  hence xI: "\<And>I. I \<in> S \<Longrightarrow> x \<in> I" by simp
-
-  from notempty have "\<exists>I0. I0 \<in> S" by blast
-  from this obtain I0 where I0S: "I0 \<in> S" by auto
-
-  interpret ideal I0 R by (rule Sideals[OF I0S])
-
-  from xI[OF I0S] have "x \<in> I0" .
-  from this and a_subset show "x \<in> carrier R" by fast
-next
   fix x y
   assume "\<forall>I\<in>S. x \<in> I"
   hence xI: "\<And>I. I \<in> S \<Longrightarrow> x \<in> I" by simp
@@ -298,6 +286,20 @@
 
   from xI[OF JS] and ycarr
       show "x \<otimes> y \<in> J" by (rule I_r_closed)
+next
+  fix x
+  assume "\<forall>I\<in>S. x \<in> I"
+  hence xI: "\<And>I. I \<in> S \<Longrightarrow> x \<in> I" by simp
+
+  from notempty have "\<exists>I0. I0 \<in> S" by blast
+  from this obtain I0 where I0S: "I0 \<in> S" by auto
+
+  interpret ideal I0 R by (rule Sideals[OF I0S])
+
+  from xI[OF I0S] have "x \<in> I0" .
+  from this and a_subset show "x \<in> carrier R" by fast
+next
+
 qed
 
 
diff -r 202d2f56560c -r 60edd70b72bd src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Tue Aug 09 22:30:33 2011 +0200
+++ b/src/HOL/Complete_Lattice.thy	Tue Aug 09 22:37:33 2011 +0200
@@ -1,6 +1,6 @@
-(*  Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel; Florian Haftmann, TU Muenchen *)
+ (*  Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel; Florian Haftmann, TU Muenchen *)
 
-header {* Complete lattices, with special focus on sets *}
+header {* Complete lattices *}
 
 theory Complete_Lattice
 imports Set
@@ -102,29 +102,29 @@
     by (simp only: dual.INF_def SUP_def)
 qed
 
-lemma INF_leI: "i \<in> A \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> f i"
+lemma INF_lower: "i \<in> A \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> f i"
   by (auto simp add: INF_def intro: Inf_lower)
 
-lemma le_SUP_I: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
+lemma INF_greatest: "(\<And>i. i \<in> A \<Longrightarrow> u \<sqsubseteq> f i) \<Longrightarrow> u \<sqsubseteq> (\<Sqinter>i\<in>A. f i)"
+  by (auto simp add: INF_def intro: Inf_greatest)
+
+lemma SUP_upper: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
   by (auto simp add: SUP_def intro: Sup_upper)
 
-lemma le_INF_I: "(\<And>i. i \<in> A \<Longrightarrow> u \<sqsubseteq> f i) \<Longrightarrow> u \<sqsubseteq> (\<Sqinter>i\<in>A. f i)"
-  by (auto simp add: INF_def intro: Inf_greatest)
-
-lemma SUP_leI: "(\<And>i. i \<in> A \<Longrightarrow> f i \<sqsubseteq> u) \<Longrightarrow> (\<Squnion>i\<in>A. f i) \<sqsubseteq> u"
+lemma SUP_least: "(\<And>i. i \<in> A \<Longrightarrow> f i \<sqsubseteq> u) \<Longrightarrow> (\<Squnion>i\<in>A. f i) \<sqsubseteq> u"
   by (auto simp add: SUP_def intro: Sup_least)
 
 lemma Inf_lower2: "u \<in> A \<Longrightarrow> u \<sqsubseteq> v \<Longrightarrow> \<Sqinter>A \<sqsubseteq> v"
   using Inf_lower [of u A] by auto
 
-lemma INF_leI2: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> u \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> u"
-  using INF_leI [of i A f] by auto
+lemma INF_lower2: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> u \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> u"
+  using INF_lower [of i A f] by auto
 
 lemma Sup_upper2: "u \<in> A \<Longrightarrow> v \<sqsubseteq> u \<Longrightarrow> v \<sqsubseteq> \<Squnion>A"
   using Sup_upper [of u A] by auto
 
-lemma le_SUP_I2: "i \<in> A \<Longrightarrow> u \<sqsubseteq> f i \<Longrightarrow> u \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
-  using le_SUP_I [of i A f] by auto
+lemma SUP_upper2: "i \<in> A \<Longrightarrow> u \<sqsubseteq> f i \<Longrightarrow> u \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
+  using SUP_upper [of i A f] by auto
 
 lemma le_Inf_iff (*[simp]*): "b \<sqsubseteq> \<Sqinter>A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)"
   by (auto intro: Inf_greatest dest: Inf_lower)
@@ -266,21 +266,21 @@
 
 lemma INF_union:
   "(\<Sqinter>i \<in> A \<union> B. M i) = (\<Sqinter>i \<in> A. M i) \<sqinter> (\<Sqinter>i\<in>B. M i)"
-  by (auto intro!: antisym INF_mono intro: le_infI1 le_infI2 le_INF_I INF_leI)
+  by (auto intro!: antisym INF_mono intro: le_infI1 le_infI2 INF_greatest INF_lower)
 
 lemma Sup_union_distrib: "\<Squnion>(A \<union> B) = \<Squnion>A \<squnion> \<Squnion>B"
   by (rule antisym) (auto intro: Sup_least Sup_upper le_supI1 le_supI2)
 
 lemma SUP_union:
   "(\<Squnion>i \<in> A \<union> B. M i) = (\<Squnion>i \<in> A. M i) \<squnion> (\<Squnion>i\<in>B. M i)"
-  by (auto intro!: antisym SUP_mono intro: le_supI1 le_supI2 SUP_leI le_SUP_I)
+  by (auto intro!: antisym SUP_mono intro: le_supI1 le_supI2 SUP_least SUP_upper)
 
 lemma INF_inf_distrib: "(\<Sqinter>a\<in>A. f a) \<sqinter> (\<Sqinter>a\<in>A. g a) = (\<Sqinter>a\<in>A. f a \<sqinter> g a)"
-  by (rule antisym) (rule le_INF_I, auto intro: le_infI1 le_infI2 INF_leI INF_mono)
+  by (rule antisym) (rule INF_greatest, auto intro: le_infI1 le_infI2 INF_lower INF_mono)
 
 lemma SUP_sup_distrib: "(\<Squnion>a\<in>A. f a) \<squnion> (\<Squnion>a\<in>A. g a) = (\<Squnion>a\<in>A. f a \<squnion> g a)"
-  by (rule antisym) (auto intro: le_supI1 le_supI2 le_SUP_I SUP_mono,
-    rule SUP_leI, auto intro: le_supI1 le_supI2 le_SUP_I SUP_mono)
+  by (rule antisym) (auto intro: le_supI1 le_supI2 SUP_upper SUP_mono,
+    rule SUP_least, auto intro: le_supI1 le_supI2 SUP_upper SUP_mono)
 
 lemma Inf_top_conv (*[simp]*) [no_atp]:
   "\<Sqinter>A = \<top> \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
@@ -324,10 +324,10 @@
   by (auto simp add: SUP_def Sup_bot_conv)
 
 lemma INF_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Sqinter>i\<in>A. f) = f"
-  by (auto intro: antisym INF_leI le_INF_I)
+  by (auto intro: antisym INF_lower INF_greatest)
 
 lemma SUP_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Squnion>i\<in>A. f) = f"
-  by (auto intro: antisym SUP_leI le_SUP_I)
+  by (auto intro: antisym SUP_upper SUP_least)
 
 lemma INF_top (*[simp]*): "(\<Sqinter>x\<in>A. \<top>) = \<top>"
   by (cases "A = {}") (simp_all add: INF_empty)
@@ -336,10 +336,10 @@
   by (cases "A = {}") (simp_all add: SUP_empty)
 
 lemma INF_commute: "(\<Sqinter>i\<in>A. \<Sqinter>j\<in>B. f i j) = (\<Sqinter>j\<in>B. \<Sqinter>i\<in>A. f i j)"
-  by (iprover intro: INF_leI le_INF_I order_trans antisym)
+  by (iprover intro: INF_lower INF_greatest order_trans antisym)
 
 lemma SUP_commute: "(\<Squnion>i\<in>A. \<Squnion>j\<in>B. f i j) = (\<Squnion>j\<in>B. \<Squnion>i\<in>A. f i j)"
-  by (iprover intro: SUP_leI le_SUP_I order_trans antisym)
+  by (iprover intro: SUP_upper SUP_least order_trans antisym)
 
 lemma INF_absorb:
   assumes "k \<in> I"
@@ -370,7 +370,7 @@
 proof -
   note `y < (\<Sqinter>i\<in>A. f i)`
   also have "(\<Sqinter>i\<in>A. f i) \<le> f i" using `i \<in> A`
-    by (rule INF_leI)
+    by (rule INF_lower)
   finally show "y < f i" .
 qed
 
@@ -378,7 +378,7 @@
   assumes "(\<Squnion>i\<in>A. f i) < y" "i \<in> A" shows "f i < y"
 proof -
   have "f i \<le> (\<Squnion>i\<in>A. f i)" using `i \<in> A`
-    by (rule le_SUP_I)
+    by (rule SUP_upper)
   also note `(\<Squnion>i\<in>A. f i) < y`
   finally show "f i < y" .
 qed
@@ -605,7 +605,7 @@
   by (simp add: Sup_fun_def)
 
 instance proof
-qed (auto simp add: le_fun_def Inf_apply Sup_apply intro: INF_leI le_SUP_I le_INF_I SUP_leI)
+qed (auto simp add: le_fun_def Inf_apply Sup_apply intro: INF_lower INF_greatest SUP_upper SUP_least)
 
 end
 
@@ -759,10 +759,10 @@
   by blast
 
 lemma INT_lower: "a \<in> A \<Longrightarrow> (\<Inter>x\<in>A. B x) \<subseteq> B a"
-  by (fact INF_leI)
+  by (fact INF_lower)
 
 lemma INT_greatest: "(\<And>x. x \<in> A \<Longrightarrow> C \<subseteq> B x) \<Longrightarrow> C \<subseteq> (\<Inter>x\<in>A. B x)"
-  by (fact le_INF_I)
+  by (fact INF_greatest)
 
 lemma INT_empty: "(\<Inter>x\<in>{}. B x) = UNIV"
   by (fact INF_empty)
@@ -947,10 +947,10 @@
   by blast
 
 lemma UN_upper: "a \<in> A \<Longrightarrow> B a \<subseteq> (\<Union>x\<in>A. B x)"
-  by (fact le_SUP_I)
+  by (fact SUP_upper)
 
 lemma UN_least: "(\<And>x. x \<in> A \<Longrightarrow> B x \<subseteq> C) \<Longrightarrow> (\<Union>x\<in>A. B x) \<subseteq> C"
-  by (fact SUP_leI)
+  by (fact SUP_least)
 
 lemma Collect_bex_eq [no_atp]: "{x. \<exists>y\<in>A. P x y} = (\<Union>y\<in>A. {x. P x y})"
   by blast
@@ -1166,9 +1166,12 @@
 
 lemmas (in complete_lattice) INFI_def = INF_def
 lemmas (in complete_lattice) SUPR_def = SUP_def
-lemmas (in complete_lattice) le_SUPI = le_SUP_I
-lemmas (in complete_lattice) le_SUPI2 = le_SUP_I2
-lemmas (in complete_lattice) le_INFI = le_INF_I
+lemmas (in complete_lattice) INF_leI = INF_lower
+lemmas (in complete_lattice) INF_leI2 = INF_lower2
+lemmas (in complete_lattice) le_INFI = INF_greatest
+lemmas (in complete_lattice) le_SUPI = SUP_upper
+lemmas (in complete_lattice) le_SUPI2 = SUP_upper2
+lemmas (in complete_lattice) SUP_leI = SUP_least
 lemmas (in complete_lattice) less_INFD = less_INF_D
 
 lemmas INFI_apply = INF_apply
diff -r 202d2f56560c -r 60edd70b72bd src/HOL/Import/HOLLight/hollight.imp
--- a/src/HOL/Import/HOLLight/hollight.imp	Tue Aug 09 22:30:33 2011 +0200
+++ b/src/HOL/Import/HOLLight/hollight.imp	Tue Aug 09 22:37:33 2011 +0200
@@ -590,7 +590,6 @@
   "UNIONS_INSERT" > "Complete_Lattice.Union_insert"
   "UNIONS_IMAGE" > "HOLLight.hollight.UNIONS_IMAGE"
   "UNIONS_GSPEC" > "HOLLight.hollight.UNIONS_GSPEC"
-  "UNIONS_2" > "Complete_Lattice.Un_eq_Union"
   "UNIONS_0" > "Complete_Lattice.Union_empty"
   "UNCURRY_def" > "HOLLight.hollight.UNCURRY_def"
   "TYDEF_recspace" > "HOLLight.hollight.TYDEF_recspace"
@@ -1596,7 +1595,6 @@
   "INTERS_INSERT" > "Complete_Lattice.Inter_insert"
   "INTERS_IMAGE" > "HOLLight.hollight.INTERS_IMAGE"
   "INTERS_GSPEC" > "HOLLight.hollight.INTERS_GSPEC"
-  "INTERS_2" > "Complete_Lattice.Int_eq_Inter"
   "INTERS_0" > "Complete_Lattice.Inter_empty"
   "INSERT_UNIV" > "HOLLight.hollight.INSERT_UNIV"
   "INSERT_UNION_EQ" > "Set.Un_insert_left"
diff -r 202d2f56560c -r 60edd70b72bd src/HOL/Number_Theory/MiscAlgebra.thy
--- a/src/HOL/Number_Theory/MiscAlgebra.thy	Tue Aug 09 22:30:33 2011 +0200
+++ b/src/HOL/Number_Theory/MiscAlgebra.thy	Tue Aug 09 22:37:33 2011 +0200
@@ -8,7 +8,7 @@
 imports
   "~~/src/HOL/Algebra/Ring"
   "~~/src/HOL/Algebra/FiniteProduct"
-begin;
+begin
 
 (* finiteness stuff *)
 
@@ -34,7 +34,7 @@
 definition units_of :: "('a, 'b) monoid_scheme => 'a monoid" where
   "units_of G == (| carrier = Units G,
      Group.monoid.mult = Group.monoid.mult G,
-     one  = one G |)";
+     one  = one G |)"
 
 (*
 
@@ -264,7 +264,7 @@
       (ALL A:C. ALL B:C. A ~= B --> A Int B = {}) |] 
    ==> finprod G f (Union C) = finprod G (finprod G f) C" 
   apply (frule finprod_UN_disjoint [of C id f])
-  apply (unfold Union_def id_def, auto)
+  apply (auto simp add: SUP_def)
 done
 
 lemma (in comm_monoid) finprod_one [rule_format]: 
diff -r 202d2f56560c -r 60edd70b72bd src/HOL/Probability/Caratheodory.thy
--- a/src/HOL/Probability/Caratheodory.thy	Tue Aug 09 22:30:33 2011 +0200
+++ b/src/HOL/Probability/Caratheodory.thy	Tue Aug 09 22:37:33 2011 +0200
@@ -6,7 +6,7 @@
 header {*Caratheodory Extension Theorem*}
 
 theory Caratheodory
-  imports Sigma_Algebra Extended_Real_Limits
+imports Sigma_Algebra "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits"
 begin
 
 lemma sums_def2:
@@ -433,8 +433,7 @@
             hence eq_fa: "f a = f (a \<inter> (\<Union>i\<in>{0..<n}. A i)) + f (a - (\<Union>i\<in>{0..<n}. A i))"
               by (simp add: lambda_system_eq UNION_in)
             have "f (a - (\<Union>i. A i)) \<le> f (a - (\<Union>i\<in>{0..<n}. A i))"
-              by (blast intro: increasingD [OF inc] UNION_eq_Union_image
-                               UNION_in U_in)
+              by (blast intro: increasingD [OF inc] UNION_in U_in)
             thus "(\<Sum>i<n. f (a \<inter> A i)) + f (a - (\<Union>i. A i)) \<le> f a"
               by (simp add: lambda_system_strong_sum pos A disj eq_fa add_left_mono atLeast0LessThan[symmetric])
           next
diff -r 202d2f56560c -r 60edd70b72bd src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Tue Aug 09 22:30:33 2011 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Tue Aug 09 22:37:33 2011 +0200
@@ -315,10 +315,10 @@
   by (auto simp add: binary_def)
 
 lemma Un_range_binary: "a \<union> b = (\<Union>i::nat. binary a b i)"
-  by (simp add: UNION_eq_Union_image range_binary_eq)
+  by (simp add: SUP_def range_binary_eq)
 
 lemma Int_range_binary: "a \<inter> b = (\<Inter>i::nat. binary a b i)"
-  by (simp add: INTER_eq_Inter_image range_binary_eq)
+  by (simp add: INF_def range_binary_eq)
 
 lemma sigma_algebra_iff2:
      "sigma_algebra M \<longleftrightarrow>
@@ -1109,7 +1109,7 @@
   done
 
 lemma UN_binaryset_eq: "(\<Union>i. binaryset A B i) = A \<union> B"
-  by (simp add: UNION_eq_Union_image range_binaryset_eq)
+  by (simp add: SUP_def range_binaryset_eq)
 
 section {* Closed CDI *}
 
diff -r 202d2f56560c -r 60edd70b72bd src/HOL/UNITY/ELT.thy
--- a/src/HOL/UNITY/ELT.thy	Tue Aug 09 22:30:33 2011 +0200
+++ b/src/HOL/UNITY/ELT.thy	Tue Aug 09 22:37:33 2011 +0200
@@ -186,9 +186,7 @@
 lemma leadsETo_Un:
      "[| F : A leadsTo[CC] C; F : B leadsTo[CC] C |] 
       ==> F : (A Un B) leadsTo[CC] C"
-apply (subst Un_eq_Union)
-apply (blast intro: leadsETo_Union)
-done
+  using leadsETo_Union [of "{A, B}" F CC C] by auto
 
 lemma single_leadsETo_I:
      "(!!x. x : A ==> F : {x} leadsTo[CC] B) ==> F : A leadsTo[CC] B"
@@ -407,9 +405,7 @@
 lemma LeadsETo_Un:
      "[| F : A LeadsTo[CC] C; F : B LeadsTo[CC] C |]  
       ==> F : (A Un B) LeadsTo[CC] C"
-apply (subst Un_eq_Union)
-apply (blast intro: LeadsETo_Union)
-done
+  using LeadsETo_Union [of "{A, B}" F CC C] by auto
 
 (*Lets us look at the starting state*)
 lemma single_LeadsETo_I:
diff -r 202d2f56560c -r 60edd70b72bd src/HOL/UNITY/ProgressSets.thy
--- a/src/HOL/UNITY/ProgressSets.thy	Tue Aug 09 22:30:33 2011 +0200
+++ b/src/HOL/UNITY/ProgressSets.thy	Tue Aug 09 22:37:33 2011 +0200
@@ -42,25 +42,21 @@
 
 lemma UN_in_lattice:
      "[|lattice L; !!i. i\<in>I ==> r i \<in> L|] ==> (\<Union>i\<in>I. r i) \<in> L"
-apply (simp add: UN_eq) 
+apply (unfold SUP_def)
 apply (blast intro: Union_in_lattice) 
 done
 
 lemma INT_in_lattice:
      "[|lattice L; !!i. i\<in>I ==> r i \<in> L|] ==> (\<Inter>i\<in>I. r i)  \<in> L"
-apply (simp add: INT_eq) 
+apply (unfold INF_def)
 apply (blast intro: Inter_in_lattice) 
 done
 
 lemma Un_in_lattice: "[|x\<in>L; y\<in>L; lattice L|] ==> x\<union>y \<in> L"
-apply (simp only: Un_eq_Union) 
-apply (blast intro: Union_in_lattice) 
-done
+  using Union_in_lattice [of "{x, y}" L] by simp
 
 lemma Int_in_lattice: "[|x\<in>L; y\<in>L; lattice L|] ==> x\<inter>y \<in> L"
-apply (simp only: Int_eq_Inter) 
-apply (blast intro: Inter_in_lattice) 
-done
+  using Inter_in_lattice [of "{x, y}" L] by simp
 
 lemma lattice_stable: "lattice {X. F \<in> stable X}"
 by (simp add: lattice_def stable_def constrains_def, blast)
diff -r 202d2f56560c -r 60edd70b72bd src/HOL/UNITY/SubstAx.thy
--- a/src/HOL/UNITY/SubstAx.thy	Tue Aug 09 22:30:33 2011 +0200
+++ b/src/HOL/UNITY/SubstAx.thy	Tue Aug 09 22:37:33 2011 +0200
@@ -85,16 +85,14 @@
 
 lemma LeadsTo_UN: 
      "(!!i. i \<in> I ==> F \<in> (A i) LeadsTo B) ==> F \<in> (\<Union>i \<in> I. A i) LeadsTo B"
-apply (simp only: Union_image_eq [symmetric])
+apply (unfold SUP_def)
 apply (blast intro: LeadsTo_Union)
 done
 
 text{*Binary union introduction rule*}
 lemma LeadsTo_Un:
      "[| F \<in> A LeadsTo C; F \<in> B LeadsTo C |] ==> F \<in> (A \<union> B) LeadsTo C"
-apply (subst Un_eq_Union)
-apply (blast intro: LeadsTo_Union)
-done
+  using LeadsTo_UN [of "{A, B}" F id C] by auto
 
 text{*Lets us look at the starting state*}
 lemma single_LeadsTo_I:
diff -r 202d2f56560c -r 60edd70b72bd src/HOL/UNITY/Transformers.thy
--- a/src/HOL/UNITY/Transformers.thy	Tue Aug 09 22:30:33 2011 +0200
+++ b/src/HOL/UNITY/Transformers.thy	Tue Aug 09 22:37:33 2011 +0200
@@ -467,7 +467,7 @@
       "single_valued act
        ==> insert (wens_single act B) (range (wens_single_finite act B)) \<subseteq> 
            wens_set (mk_program (init, {act}, allowed)) B"
-apply (simp add: wens_single_eq_Union UN_eq) 
+apply (simp add: SUP_def image_def wens_single_eq_Union) 
 apply (blast intro: wens_set.Union wens_single_finite_in_wens_set)
 done
 
diff -r 202d2f56560c -r 60edd70b72bd src/HOL/UNITY/WFair.thy
--- a/src/HOL/UNITY/WFair.thy	Tue Aug 09 22:30:33 2011 +0200
+++ b/src/HOL/UNITY/WFair.thy	Tue Aug 09 22:37:33 2011 +0200
@@ -211,9 +211,7 @@
 text{*Binary union introduction rule*}
 lemma leadsTo_Un:
      "[| F \<in> A leadsTo C; F \<in> B leadsTo C |] ==> F \<in> (A \<union> B) leadsTo C"
-apply (subst Un_eq_Union)
-apply (blast intro: leadsTo_Union)
-done
+  using leadsTo_Union [of "{A, B}" F C] by auto
 
 lemma single_leadsTo_I: 
      "(!!x. x \<in> A ==> F \<in> {x} leadsTo B) ==> F \<in> A leadsTo B"
diff -r 202d2f56560c -r 60edd70b72bd src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Tue Aug 09 22:30:33 2011 +0200
+++ b/src/Pure/Syntax/parser.ML	Tue Aug 09 22:37:33 2011 +0200
@@ -747,7 +747,7 @@
   in get_prods (connected_with chains nts nts) [] end;
 
 
-fun PROCESSS ctxt warned prods chains Estate i c states =
+fun PROCESSS ctxt prods chains Estate i c states =
   let
     fun all_prods_for nt = prods_for prods chains true c [nt];
 
@@ -773,14 +773,6 @@
                         val tk_prods = all_prods_for nt;
                         val States' = mk_states i min_prec nt (get_RHS min_prec tk_prods);
                       in (Inttab.update (nt, (min_prec, [])) used, States') end);
-
-                val _ =
-                  if not (! warned) andalso
-                     length new_states + length States > Config.get ctxt branching_level then
-                    (Context_Position.if_visible ctxt warning
-                      "Currently parsed expression could be extremely ambiguous";
-                     warned := true)
-                  else ();
               in
                 processS used' (new_states @ States) (S :: Si, Sii)
               end
@@ -803,7 +795,7 @@
   in processS Inttab.empty states ([], []) end;
 
 
-fun produce ctxt warned prods tags chains stateset i indata prev_token =
+fun produce ctxt prods tags chains stateset i indata prev_token =
   (case Array.sub (stateset, i) of
     [] =>
       let
@@ -821,10 +813,10 @@
         [] => s
       | c :: cs =>
           let
-            val (si, sii) = PROCESSS ctxt warned prods chains stateset i c s;
+            val (si, sii) = PROCESSS ctxt prods chains stateset i c s;
             val _ = Array.update (stateset, i, si);
             val _ = Array.update (stateset, i + 1, sii);
-          in produce ctxt warned prods tags chains stateset (i + 1) cs c end));
+          in produce ctxt prods tags chains stateset (i + 1) cs c end));
 
 
 fun get_trees states = map_filter (fn (_, _, [pt], _, _, _) => SOME pt | _ => NONE) states;
@@ -841,7 +833,7 @@
     val _ = Array.update (Estate, 0, S0);
   in
     get_trees
-      (produce ctxt (Unsynchronized.ref false) prods tags chains Estate 0 indata Lexicon.eof)
+      (produce ctxt prods tags chains Estate 0 indata Lexicon.eof)
   end;