# HG changeset patch
# User wenzelm
# Date 1369499438 -7200
# Node ID 893b15200ec1ee0e167186c90ed82a873c5485bd
# Parent  eff000cab70f21ddca804bd95c90f1460b94f39b# Parent  9943f8067f11d5a168d656535e35954bb9ecd962
merged

diff -r 9943f8067f11 -r 893b15200ec1 NEWS
--- a/NEWS	Sat May 25 17:40:44 2013 +0200
+++ b/NEWS	Sat May 25 18:30:38 2013 +0200
@@ -61,6 +61,9 @@
 
 *** HOL ***
 
+* Weaker precendence of syntax for big intersection and union on sets,
+in accordance with corresponding lattice operations.  INCOMPATIBILITY.
+
 * Nested case expressions are now translated in a separate check
   phase rather than during parsing. The data for case combinators
   is separated from the datatype package. The declaration attribute
diff -r 9943f8067f11 -r 893b15200ec1 src/HOL/BNF/BNF_Comp.thy
--- a/src/HOL/BNF/BNF_Comp.thy	Sat May 25 17:40:44 2013 +0200
+++ b/src/HOL/BNF/BNF_Comp.thy	Sat May 25 18:30:38 2013 +0200
@@ -24,7 +24,7 @@
   assumes fbd_Card_order: "Card_order fbd" and
     fset_bd: "\<And>x. |fset x| \<le>o fbd" and
     gset_bd: "\<And>x. |gset x| \<le>o gbd"
-  shows "|\<Union>fset ` gset x| \<le>o gbd *c fbd"
+  shows "|\<Union>(fset ` gset x)| \<le>o gbd *c fbd"
 apply (subst sym[OF SUP_def])
 apply (rule ordLeq_transitive)
 apply (rule card_of_UNION_Sigma)
@@ -42,10 +42,10 @@
 apply (rule Card_order_cprod)
 done
 
-lemma Union_image_insert: "\<Union>f ` insert a B = f a \<union> \<Union>f ` B"
+lemma Union_image_insert: "\<Union>(f ` insert a B) = f a \<union> \<Union>(f ` B)"
 by simp
 
-lemma Union_image_empty: "A \<union> \<Union>f ` {} = A"
+lemma Union_image_empty: "A \<union> \<Union>(f ` {}) = A"
 by simp
 
 lemma image_o_collect: "collect ((\<lambda>f. image g o f) ` F) = image g o collect F"
@@ -54,10 +54,10 @@
 lemma conj_subset_def: "A \<subseteq> {x. P x \<and> Q x} = (A \<subseteq> {x. P x} \<and> A \<subseteq> {x. Q x})"
 by blast
 
-lemma UN_image_subset: "\<Union>f ` g x \<subseteq> X = (g x \<subseteq> {x. f x \<subseteq> X})"
+lemma UN_image_subset: "\<Union>(f ` g x) \<subseteq> X = (g x \<subseteq> {x. f x \<subseteq> X})"
 by blast
 
-lemma comp_set_bd_Union_o_collect: "|\<Union>\<Union>(\<lambda>f. f x) ` X| \<le>o hbd \<Longrightarrow> |(Union \<circ> collect X) x| \<le>o hbd"
+lemma comp_set_bd_Union_o_collect: "|\<Union>\<Union>((\<lambda>f. f x) ` X)| \<le>o hbd \<Longrightarrow> |(Union \<circ> collect X) x| \<le>o hbd"
 by (unfold o_apply collect_def SUP_def)
 
 lemma wpull_cong:
diff -r 9943f8067f11 -r 893b15200ec1 src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Sat May 25 17:40:44 2013 +0200
+++ b/src/HOL/Complete_Lattices.thy	Sat May 25 18:30:38 2013 +0200
@@ -751,7 +751,7 @@
   "Inter S \<equiv> \<Sqinter>S"
   
 notation (xsymbols)
-  Inter  ("\<Inter>_" [90] 90)
+  Inter  ("\<Inter>_" [900] 900)
 
 lemma Inter_eq:
   "\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}"
@@ -934,7 +934,7 @@
   "Union S \<equiv> \<Squnion>S"
 
 notation (xsymbols)
-  Union  ("\<Union>_" [90] 90)
+  Union  ("\<Union>_" [900] 900)
 
 lemma Union_eq:
   "\<Union>A = {x. \<exists>B \<in> A. x \<in> B}"
diff -r 9943f8067f11 -r 893b15200ec1 src/HOL/Hoare_Parallel/OG_Tran.thy
--- a/src/HOL/Hoare_Parallel/OG_Tran.thy	Sat May 25 17:40:44 2013 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Tran.thy	Sat May 25 18:30:38 2013 +0200
@@ -90,13 +90,13 @@
   "ann_sem c \<equiv> \<lambda>s. {t. (Some c, s) -*\<rightarrow> (None, t)}"
 
 definition ann_SEM :: "'a ann_com \<Rightarrow> 'a set \<Rightarrow> 'a set" where
-  "ann_SEM c S \<equiv> \<Union>ann_sem c ` S"  
+  "ann_SEM c S \<equiv> \<Union>(ann_sem c ` S)"
 
 definition sem :: "'a com \<Rightarrow> 'a \<Rightarrow> 'a set" where
   "sem c \<equiv> \<lambda>s. {t. \<exists>Ts. (c, s) -P*\<rightarrow> (Parallel Ts, t) \<and> All_None Ts}"
 
 definition SEM :: "'a com \<Rightarrow> 'a set \<Rightarrow> 'a set" where
-  "SEM c S \<equiv> \<Union>sem c ` S "
+  "SEM c S \<equiv> \<Union>(sem c ` S)"
 
 abbreviation Omega :: "'a com"    ("\<Omega>" 63)
   where "\<Omega> \<equiv> While UNIV UNIV (Basic id)"
diff -r 9943f8067f11 -r 893b15200ec1 src/HOL/List.thy
--- a/src/HOL/List.thy	Sat May 25 17:40:44 2013 +0200
+++ b/src/HOL/List.thy	Sat May 25 18:30:38 2013 +0200
@@ -4312,7 +4312,7 @@
   moreover have "\<And>i. i \<in>Collect (?k_list k) \<Longrightarrow> card (A - set i) = card A - k"
     by (simp add: card_Diff_subset distinct_card)
   moreover have "{xs. ?k_list (Suc k) xs} =
-      (\<lambda>(xs, n). n#xs) ` \<Union>(\<lambda>xs. {xs} \<times> (A - set xs)) ` {xs. ?k_list k xs}"
+      (\<lambda>(xs, n). n#xs) ` \<Union>((\<lambda>xs. {xs} \<times> (A - set xs)) ` {xs. ?k_list k xs})"
     by (auto simp: length_Suc_conv)
   moreover
   have "Suc (card A - Suc k) = card A - k" using Suc.prems by simp
diff -r 9943f8067f11 -r 893b15200ec1 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Sat May 25 17:40:44 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Sat May 25 18:30:38 2013 +0200
@@ -1015,7 +1015,7 @@
     apply (rule that[of "d \<union> p"])
   proof -
     have *: "\<And>s f t. s \<noteq> {} \<Longrightarrow> (\<forall>i\<in>s. f i \<union> i = t) \<Longrightarrow> t = \<Inter> (f ` s) \<union> (\<Union>s)" by auto
-    have *: "{a..b} = \<Inter> (\<lambda>i. \<Union>(q i - {i})) ` p \<union> \<Union>p"
+    have *: "{a..b} = \<Inter> ((\<lambda>i. \<Union>(q i - {i})) ` p) \<union> \<Union>p"
       apply (rule *[OF False])
     proof
       fix i
@@ -1032,7 +1032,7 @@
       fix k
       assume k: "k\<in>p"
       have *: "\<And>u t s. u \<subseteq> s \<Longrightarrow> s \<inter> t = {} \<Longrightarrow> u \<inter> t = {}" by auto
-      show "interior (\<Inter>(\<lambda>i. \<Union>(q i - {i})) ` p) \<inter> interior k = {}"
+      show "interior (\<Inter> ((\<lambda>i. \<Union>(q i - {i})) ` p)) \<inter> interior k = {}"
         apply (rule *[of _ "interior (\<Union>(q k - {k}))"])
         defer
         apply (subst Int_commute)
@@ -1044,7 +1044,7 @@
         show "\<forall>t\<in>q k - {k}. interior k \<inter> interior t = {}"
           using qk(5) using q(2)[OF k] by auto
         have *: "\<And>x s. x \<in> s \<Longrightarrow> \<Inter>s \<subseteq> x" by auto
-        show "interior (\<Inter>(\<lambda>i. \<Union>(q i - {i})) ` p) \<subseteq> interior (\<Union>(q k - {k}))"
+        show "interior (\<Inter> ((\<lambda>i. \<Union>(q i - {i})) ` p)) \<subseteq> interior (\<Union>(q k - {k}))"
           apply (rule interior_mono *)+
           using k by auto
       qed
@@ -1131,7 +1131,7 @@
 lemma elementary_union_interval: assumes "p division_of \<Union>p"
   obtains q where "q division_of ({a..b::'a::ordered_euclidean_space} \<union> \<Union>p)" proof-
   note assm=division_ofD[OF assms]
-  have lem1:"\<And>f s. \<Union>\<Union> (f ` s) = \<Union>(\<lambda>x.\<Union>(f x)) ` s" by auto
+  have lem1:"\<And>f s. \<Union>\<Union> (f ` s) = \<Union>((\<lambda>x.\<Union>(f x)) ` s)" by auto
   have lem2:"\<And>f s. f \<noteq> {} \<Longrightarrow> \<Union>{s \<union> t |t. t \<in> f} = s \<union> \<Union>f" by auto
 { presume "p={} \<Longrightarrow> thesis" "{a..b} = {} \<Longrightarrow> thesis" "{a..b} \<noteq> {} \<Longrightarrow> interior {a..b} = {} \<Longrightarrow> thesis"
     "p\<noteq>{} \<Longrightarrow> interior {a..b}\<noteq>{} \<Longrightarrow> {a..b} \<noteq> {} \<Longrightarrow> thesis"
@@ -1282,7 +1282,7 @@
 
 lemma division_of_tagged_division: assumes"s tagged_division_of i"  shows "(snd ` s) division_of i"
 proof(rule division_ofI) note assm=tagged_division_ofD[OF assms]
-  show "\<Union>snd ` s = i" "finite (snd ` s)" using assm by auto
+  show "\<Union>(snd ` s) = i" "finite (snd ` s)" using assm by auto
   fix k assume k:"k \<in> snd ` s" then obtain xk where xk:"(xk, k) \<in> s" by auto
   thus  "k \<subseteq> i" "k \<noteq> {}" "\<exists>a b. k = {a..b}" using assm apply- by fastforce+
   fix k' assume k':"k' \<in> snd ` s" "k \<noteq> k'" from this(1) obtain xk' where xk':"(xk', k') \<in> s" by auto
@@ -1292,9 +1292,9 @@
 lemma partial_division_of_tagged_division: assumes "s tagged_partial_division_of i"
   shows "(snd ` s) division_of \<Union>(snd ` s)"
 proof(rule division_ofI) note assm=tagged_partial_division_ofD[OF assms]
-  show "finite (snd ` s)" "\<Union>snd ` s = \<Union>snd ` s" using assm by auto
+  show "finite (snd ` s)" "\<Union>(snd ` s) = \<Union>(snd ` s)" using assm by auto
   fix k assume k:"k \<in> snd ` s" then obtain xk where xk:"(xk, k) \<in> s" by auto
-  thus "k\<noteq>{}" "\<exists>a b. k = {a..b}" "k \<subseteq> \<Union>snd ` s" using assm by auto
+  thus "k\<noteq>{}" "\<exists>a b. k = {a..b}" "k \<subseteq> \<Union>(snd ` s)" using assm by auto
   fix k' assume k':"k' \<in> snd ` s" "k \<noteq> k'" from this(1) obtain xk' where xk':"(xk', k') \<in> s" by auto
   thus "interior k \<inter> interior k' = {}" apply-apply(rule assm(5)) apply(rule xk xk')+ using k' by auto
 qed
@@ -1355,13 +1355,13 @@
   shows "\<Union>(pfn ` iset) tagged_division_of (\<Union>iset)"
 proof(rule tagged_division_ofI)
   note assm = tagged_division_ofD[OF assms(2)[rule_format]]
-  show "finite (\<Union>pfn ` iset)" apply(rule finite_Union) using assms by auto
-  have "\<Union>{k. \<exists>x. (x, k) \<in> \<Union>pfn ` iset} = \<Union>(\<lambda>i. \<Union>{k. \<exists>x. (x, k) \<in> pfn i}) ` iset" by blast 
+  show "finite (\<Union>(pfn ` iset))" apply(rule finite_Union) using assms by auto
+  have "\<Union>{k. \<exists>x. (x, k) \<in> \<Union>(pfn ` iset)} = \<Union>((\<lambda>i. \<Union>{k. \<exists>x. (x, k) \<in> pfn i}) ` iset)" by blast 
   also have "\<dots> = \<Union>iset" using assm(6) by auto
-  finally show "\<Union>{k. \<exists>x. (x, k) \<in> \<Union>pfn ` iset} = \<Union>iset" . 
-  fix x k assume xk:"(x,k)\<in>\<Union>pfn ` iset" then obtain i where i:"i \<in> iset" "(x, k) \<in> pfn i" by auto
+  finally show "\<Union>{k. \<exists>x. (x, k) \<in> \<Union>(pfn ` iset)} = \<Union>iset" . 
+  fix x k assume xk:"(x,k)\<in>\<Union>(pfn ` iset)" then obtain i where i:"i \<in> iset" "(x, k) \<in> pfn i" by auto
   show "x\<in>k" "\<exists>a b. k = {a..b}" "k \<subseteq> \<Union>iset" using assm(2-4)[OF i] using i(1) by auto
-  fix x' k' assume xk':"(x',k')\<in>\<Union>pfn ` iset" "(x, k) \<noteq> (x', k')" then obtain i' where i':"i' \<in> iset" "(x', k') \<in> pfn i'" by auto
+  fix x' k' assume xk':"(x',k')\<in>\<Union>(pfn ` iset)" "(x, k) \<noteq> (x', k')" then obtain i' where i':"i' \<in> iset" "(x', k') \<in> pfn i'" by auto
   have *:"\<And>a b. i\<noteq>i' \<Longrightarrow> a\<subseteq> i \<Longrightarrow> b\<subseteq> i' \<Longrightarrow> interior a \<inter> interior b = {}" using i(1) i'(1)
     using assms(3)[rule_format] interior_mono by blast
   show "interior k \<inter> interior k' = {}" apply(cases "i=i'")
@@ -4975,7 +4975,7 @@
   shows "norm(setsum (\<lambda>(x,k). content k *\<^sub>R f x - integral k f) p) \<le> e" (is "?x \<le> e")
 proof-  { presume "\<And>k. 0<k \<Longrightarrow> ?x \<le> e + k" thus ?thesis by (blast intro: field_le_epsilon) }
   fix k::real assume k:"k>0" note p' = tagged_partial_division_ofD[OF p(1)]
-  have "\<Union>snd ` p \<subseteq> {a..b}" using p'(3) by fastforce
+  have "\<Union>(snd ` p) \<subseteq> {a..b}" using p'(3) by fastforce
   note partial_division_of_tagged_division[OF p(1)] this
   from partial_division_extend_interval[OF this] guess q . note q=this and q' = division_ofD[OF this(2)]
   def r \<equiv> "q - snd ` p" have "snd ` p \<inter> r = {}" unfolding r_def by auto
@@ -4994,11 +4994,11 @@
     thus ?case apply(rule_tac x=qq in exI) using dd(2)[of qq] unfolding fine_inter uv by auto qed
   from bchoice[OF this] guess qq .. note qq=this[rule_format]
 
-  let ?p = "p \<union> \<Union>qq ` r" have "norm ((\<Sum>(x, k)\<in>?p. content k *\<^sub>R f x) - integral {a..b} f) < e"
+  let ?p = "p \<union> \<Union>(qq ` r)" have "norm ((\<Sum>(x, k)\<in>?p. content k *\<^sub>R f x) - integral {a..b} f) < e"
     apply(rule assms(4)[rule_format])
   proof show "d fine ?p" apply(rule fine_union,rule p) apply(rule fine_unions) using qq by auto 
     note * = tagged_partial_division_of_union_self[OF p(1)]
-    have "p \<union> \<Union>qq ` r tagged_division_of \<Union>snd ` p \<union> \<Union>r"
+    have "p \<union> \<Union>(qq ` r) tagged_division_of \<Union>(snd ` p) \<union> \<Union>r"
     proof(rule tagged_division_union[OF * tagged_division_unions])
       show "finite r" by fact case goal2 thus ?case using qq by auto
     next case goal3 thus ?case apply(rule,rule,rule) apply(rule q'(5)) unfolding r_def by auto
@@ -5006,11 +5006,11 @@
         apply(rule,rule q') defer apply(rule,subst Int_commute) 
         apply(rule inter_interior_unions_intervals) apply(rule finite_imageI,rule p',rule) defer
         apply(rule,rule q') using q(1) p' unfolding r_def by auto qed
-    moreover have "\<Union>snd ` p \<union> \<Union>r = {a..b}" "{qq i |i. i \<in> r} = qq ` r"
+    moreover have "\<Union>(snd ` p) \<union> \<Union>r = {a..b}" "{qq i |i. i \<in> r} = qq ` r"
       unfolding Union_Un_distrib[THEN sym] r_def using q by auto
     ultimately show "?p tagged_division_of {a..b}" by fastforce qed
 
-  hence "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>\<Union>qq ` r. content k *\<^sub>R f x) -
+  hence "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>\<Union>(qq ` r). content k *\<^sub>R f x) -
     integral {a..b} f) < e" apply(subst setsum_Un_zero[THEN sym]) apply(rule p') prefer 3 
     apply assumption apply rule apply(rule finite_imageI,rule r) apply safe apply(drule qq)
   proof- fix x l k assume as:"(x,l)\<in>p" "(x,l)\<in>qq k" "k\<in>r"
diff -r 9943f8067f11 -r 893b15200ec1 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sat May 25 17:40:44 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sat May 25 18:30:38 2013 +0200
@@ -220,7 +220,7 @@
     fix a assume "a \<in> A"
     thus "x \<in> a" "open a" using A'(4)[OF open_UNIV] by (auto simp: A_def intro: A' from_nat_into)
   next
-    let ?int = "\<lambda>N. \<Inter>from_nat_into A' ` N"
+    let ?int = "\<lambda>N. \<Inter>(from_nat_into A' ` N)"
     fix a b assume "a \<in> A" "b \<in> A"
     then obtain N M where "a = ?int N" "b = ?int M" "finite (N \<union> M)" by (auto simp: A_def)
     thus "a \<inter> b \<in> A" by (auto simp: A_def intro!: image_eqI[where x="N \<union> M"])
@@ -2617,7 +2617,7 @@
 proof (safe intro!: compact_eq_heine_borel[THEN iffD2])
   fix A assume "compact U" and A: "\<forall>a\<in>A. closed a" "U \<inter> \<Inter>A = {}"
     and fi: "\<forall>B \<subseteq> A. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {}"
-  from A have "(\<forall>a\<in>uminus`A. open a) \<and> U \<subseteq> \<Union>uminus`A"
+  from A have "(\<forall>a\<in>uminus`A. open a) \<and> U \<subseteq> \<Union>(uminus`A)"
     by auto
   with `compact U` obtain B where "B \<subseteq> A" "finite (uminus`B)" "U \<subseteq> \<Union>(uminus`B)"
     unfolding compact_eq_heine_borel by (metis subset_image_iff)
@@ -2627,7 +2627,7 @@
   fix A assume ?R and cover: "\<forall>a\<in>A. open a" "U \<subseteq> \<Union>A"
   from cover have "U \<inter> \<Inter>(uminus`A) = {}" "\<forall>a\<in>uminus`A. closed a"
     by auto
-  with `?R` obtain B where "B \<subseteq> A" "finite (uminus`B)" "U \<inter> \<Inter>uminus`B = {}"
+  with `?R` obtain B where "B \<subseteq> A" "finite (uminus`B)" "U \<inter> \<Inter>(uminus`B) = {}"
     by (metis subset_image_iff)
   then show "\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T"
     by  (auto intro!: exI[of _ B] inj_setminus dest: finite_imageD)
@@ -3041,7 +3041,7 @@
   assumes "seq_compact s"
   shows "\<forall>e>0. \<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` k))"
 proof(rule, rule, rule ccontr)
-  fix e::real assume "e>0" and assm:"\<not> (\<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> \<Union>(\<lambda>x. ball x e) ` k)"
+  fix e::real assume "e>0" and assm:"\<not> (\<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> \<Union>((\<lambda>x. ball x e) ` k))"
   def x \<equiv> "helper_1 s e"
   { fix n
     have "x n \<in> s \<and> (\<forall>m<n. \<not> dist (x m) (x n) < e)"
@@ -4586,7 +4586,7 @@
     moreover with c have "(\<Inter>y\<in>D. a y) \<times> t \<subseteq> (\<Union>y\<in>D. c y)"
       by (fastforce simp: subset_eq)
     ultimately show "\<exists>a. open a \<and> x \<in> a \<and> (\<exists>d\<subseteq>C. finite d \<and> a \<times> t \<subseteq> \<Union>d)"
-      using c by (intro exI[of _ "c`D"] exI[of _ "\<Inter>a`D"] conjI) (auto intro!: open_INT)
+      using c by (intro exI[of _ "c`D"] exI[of _ "\<Inter>(a`D)"] conjI) (auto intro!: open_INT)
   qed
   then obtain a d where a: "\<forall>x\<in>s. open (a x)" "s \<subseteq> (\<Union>x\<in>s. a x)"
     and d: "\<And>x. x \<in> s \<Longrightarrow> d x \<subseteq> C \<and> finite (d x) \<and> a x \<times> t \<subseteq> \<Union>d x"
diff -r 9943f8067f11 -r 893b15200ec1 src/HOL/Probability/Caratheodory.thy
--- a/src/HOL/Probability/Caratheodory.thy	Sat May 25 17:40:44 2013 +0200
+++ b/src/HOL/Probability/Caratheodory.thy	Sat May 25 18:30:38 2013 +0200
@@ -707,9 +707,9 @@
   assumes A: "\<And>i. i \<in> I \<Longrightarrow> A i \<in> M" "disjoint_family_on A I" "finite I" "UNION I A \<in> M"
   shows "f (UNION I A) = (\<Sum>i\<in>I. f (A i))"
 proof -
-  have "A`I \<subseteq> M" "disjoint (A`I)" "finite (A`I)" "\<Union>A`I \<in> M"
+  have "A`I \<subseteq> M" "disjoint (A`I)" "finite (A`I)" "\<Union>(A`I) \<in> M"
     using A unfolding SUP_def by (auto simp: disjoint_family_on_disjoint_image)
-  with `volume M f` have "f (\<Union>A`I) = (\<Sum>a\<in>A`I. f a)"
+  with `volume M f` have "f (\<Union>(A`I)) = (\<Sum>a\<in>A`I. f a)"
     unfolding volume_def by blast
   also have "\<dots> = (\<Sum>i\<in>I. f (A i))"
   proof (subst setsum_reindex_nonzero)
diff -r 9943f8067f11 -r 893b15200ec1 src/HOL/Probability/Radon_Nikodym.thy
--- a/src/HOL/Probability/Radon_Nikodym.thy	Sat May 25 17:40:44 2013 +0200
+++ b/src/HOL/Probability/Radon_Nikodym.thy	Sat May 25 18:30:38 2013 +0200
@@ -571,9 +571,9 @@
     show "(SUP i. emeasure M (?O i)) \<le> ?a" unfolding SUP_def
     proof (safe intro!: Sup_mono, unfold bex_simps)
       fix i
-      have *: "(\<Union>Q' ` {..i}) = ?O i" by auto
+      have *: "(\<Union>(Q' ` {..i})) = ?O i" by auto
       then show "\<exists>x. (x \<in> sets M \<and> N x \<noteq> \<infinity>) \<and>
-        emeasure M (\<Union>Q' ` {..i}) \<le> emeasure M x"
+        emeasure M (\<Union>(Q' ` {..i})) \<le> emeasure M x"
         using O_in_G[of i] by (auto intro!: exI[of _ "?O i"])
     qed
   qed
diff -r 9943f8067f11 -r 893b15200ec1 src/HOL/Probability/Regularity.thy
--- a/src/HOL/Probability/Regularity.thy	Sat May 25 17:40:44 2013 +0200
+++ b/src/HOL/Probability/Regularity.thy	Sat May 25 18:30:38 2013 +0200
@@ -209,8 +209,8 @@
       from nat_approx_posE[OF this] guess n . note n = this
       let ?k = "from_nat_into X ` {0..k e (Suc n)}"
       have "finite ?k" by simp
-      moreover have "K \<subseteq> \<Union>(\<lambda>x. ball x e') ` ?k" unfolding K_def B_def using n by force
-      ultimately show "\<exists>k. finite k \<and> K \<subseteq> \<Union>(\<lambda>x. ball x e') ` k" by blast
+      moreover have "K \<subseteq> \<Union>((\<lambda>x. ball x e') ` ?k)" unfolding K_def B_def using n by force
+      ultimately show "\<exists>k. finite k \<and> K \<subseteq> \<Union>((\<lambda>x. ball x e') ` k)" by blast
     qed
     ultimately
     show "?thesis e " by (auto simp: sU)
diff -r 9943f8067f11 -r 893b15200ec1 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Sat May 25 17:40:44 2013 +0200
+++ b/src/Pure/Isar/expression.ML	Sat May 25 18:30:38 2013 +0200
@@ -810,29 +810,34 @@
 
 local
 
-fun read_with_extended_syntax parse_prop deps ctxt props =
+(* reading *)
+
+fun read_with_extended_syntax prep_prop deps ctxt props =
   let
     val deps_ctxt = fold Locale.activate_declarations deps ctxt;
   in
-    map (parse_prop deps_ctxt o snd) props |> Syntax.check_terms deps_ctxt
+    map (prep_prop deps_ctxt o snd) props |> Syntax.check_terms deps_ctxt
       |> Variable.export_terms deps_ctxt ctxt
   end;
 
-fun read_interpretation prep_expr parse_prop prep_attr expression raw_eqns initial_ctxt =
+fun read_interpretation prep_expr prep_prop prep_attr expression raw_eqns initial_ctxt =
   let
     val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt;
-    val eqns = read_with_extended_syntax parse_prop deps expr_ctxt raw_eqns;
+    val eqns = read_with_extended_syntax prep_prop deps expr_ctxt raw_eqns;
     val attrss = map (apsnd (map (prep_attr (Proof_Context.theory_of initial_ctxt))) o fst) raw_eqns;
     val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
     val export' = Variable.export_morphism goal_ctxt expr_ctxt;
   in (((propss, deps, export, export'), (eqns, attrss)), goal_ctxt) end;
 
+
+(* generic interpretation machinery *)
+
 fun meta_rewrite eqns ctxt = (map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns), ctxt);
 
 fun note_eqns_register note activate deps witss eqns attrss export export' ctxt =
   let
-    val facts = 
-      (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns);
+    val facts = map2 (fn attrs => fn eqn =>
+      (attrs, [([Morphism.thm (export' $> export) eqn], [])])) attrss eqns;
     val (eqns', ctxt') = ctxt
       |> note Thm.lemmaK facts
       |-> meta_rewrite;
@@ -845,24 +850,22 @@
     |> fold activate' dep_morphs
   end;
 
-fun generic_interpretation prep_expr parse_prop prep_attr setup_proof note add_registration
+fun generic_interpretation prep_expr prep_prop prep_attr setup_proof note activate
     expression raw_eqns initial_ctxt = 
   let
     val (((propss, deps, export, export'), (eqns, attrss)), goal_ctxt) = 
-      read_interpretation prep_expr parse_prop prep_attr expression raw_eqns initial_ctxt;
+      read_interpretation prep_expr prep_prop prep_attr expression raw_eqns initial_ctxt;
     fun after_qed witss eqns =
-      note_eqns_register note add_registration deps witss eqns attrss export export';
+      note_eqns_register note activate deps witss eqns attrss export export';
   in setup_proof after_qed propss eqns goal_ctxt end;
 
-val activate_proof = Context.proof_map ooo Locale.add_registration;
-val activate_local_theory = Local_Theory.surface_target ooo activate_proof;
-val add_registration = Local_Theory.raw_theory o Context.theory_map ooo Locale.add_registration;
-fun add_dependency locale dep_morph mixin export =
-  (Local_Theory.raw_theory ooo Locale.add_dependency locale) dep_morph mixin export
-  #> activate_local_theory dep_morph mixin export;
-fun add_dependency_global locale = Proof_Context.background_theory ooo Locale.add_dependency locale;
+
+(* various flavours of interpretation *)
 
-fun gen_interpret prep_expr parse_prop prep_attr expression raw_eqns int state =
+fun assert_not_theory lthy = if Named_Target.is_theory lthy
+  then error "Not possible on level of global theory" else ();
+
+fun gen_interpret prep_expr prep_prop prep_attr expression raw_eqns int state =
   let
     val _ = Proof.assert_forward_or_chain state;
     val ctxt = Proof.context_of state;
@@ -870,43 +873,40 @@
     fun setup_proof after_qed propss eqns goal_ctxt = 
       Element.witness_local_proof_eqs (lift_after_qed after_qed) "interpret" propss eqns goal_ctxt int state;
   in
-    generic_interpretation prep_expr parse_prop prep_attr setup_proof
-      Attrib.local_notes activate_proof expression raw_eqns ctxt
+    generic_interpretation prep_expr prep_prop prep_attr setup_proof
+      Attrib.local_notes (Context.proof_map ooo Locale.add_registration) expression raw_eqns ctxt
   end;
 
-fun gen_interpretation prep_expr parse_prop prep_attr expression raw_eqns lthy =
+fun gen_interpretation prep_expr prep_prop prep_attr expression raw_eqns lthy =
+  if Named_Target.is_theory lthy
+  then 
+    lthy
+    |> generic_interpretation prep_expr prep_prop prep_attr Element.witness_proof_eqs
+        Local_Theory.notes_kind Local_Theory.add_registration expression raw_eqns
+  else
+    lthy
+    |> generic_interpretation prep_expr prep_prop prep_attr Element.witness_proof_eqs
+        Local_Theory.notes_kind Local_Theory.activate expression raw_eqns;
+
+fun gen_sublocale prep_expr prep_prop prep_attr expression raw_eqns lthy =
   let
-    val is_theory = Option.map #target (Named_Target.peek lthy) = SOME ""
-      andalso Local_Theory.level lthy = 1;
-    val activate = if is_theory then add_registration else activate_local_theory;
-    val mark_brittle = if is_theory then I else Local_Theory.mark_brittle;
+    val _ = assert_not_theory lthy;
+    val locale = Named_Target.the_name lthy;
   in
     lthy
-    |> mark_brittle
-    |> generic_interpretation prep_expr parse_prop prep_attr Element.witness_proof_eqs
-        Local_Theory.notes_kind activate expression raw_eqns
-  end;
-
-fun gen_sublocale prep_expr parse_prop prep_attr expression raw_eqns lthy =
-  let
-    val locale =
-      case Option.map #target (Named_Target.peek lthy) of
-          SOME locale => locale
-        | _ => error "Not in a locale target";
-  in
-    lthy
-    |> generic_interpretation prep_expr parse_prop prep_attr Element.witness_proof_eqs
-        Local_Theory.notes_kind (add_dependency locale) expression raw_eqns
+    |> generic_interpretation prep_expr prep_prop prep_attr Element.witness_proof_eqs
+        Local_Theory.notes_kind (Local_Theory.add_dependency locale) expression raw_eqns
   end;
   
-fun gen_sublocale_global prep_expr prep_loc parse_prop prep_attr before_exit raw_locale expression raw_eqns thy =
+fun gen_sublocale_global prep_expr prep_loc prep_prop prep_attr before_exit raw_locale expression raw_eqns thy =
   let
     val locale = prep_loc thy raw_locale;
+    val add_dependency_global = Proof_Context.background_theory ooo Locale.add_dependency locale;
   in
     thy
     |> Named_Target.init before_exit locale
-    |> generic_interpretation prep_expr parse_prop prep_attr Element.witness_proof_eqs
-        Local_Theory.notes_kind (add_dependency_global locale) expression raw_eqns
+    |> generic_interpretation prep_expr prep_prop prep_attr Element.witness_proof_eqs
+        Local_Theory.notes_kind add_dependency_global expression raw_eqns
   end;
 
 in
@@ -914,27 +914,22 @@
 fun permanent_interpretation expression raw_eqns lthy =
   let
     val _ = Local_Theory.assert_bottom true lthy;
-    val target = case Named_Target.peek lthy of
-          SOME { target, ... } => target
-        | NONE => error "Not in a named target";
-    val is_theory = (target = "");
-    val activate = if is_theory then add_registration else add_dependency target;
+    val target = Named_Target.the_name lthy;
+    val subscribe = if target = "" then Local_Theory.add_registration
+      else Local_Theory.add_dependency target;
   in
     lthy
     |> generic_interpretation cert_goal_expression (K I) (K I) Element.witness_proof_eqs
-        Local_Theory.notes_kind activate expression raw_eqns
+        Local_Theory.notes_kind subscribe expression raw_eqns
   end;
 
 fun ephemeral_interpretation expression raw_eqns lthy =
   let
-    val _ = if Option.map #target (Named_Target.peek lthy) = SOME ""
-      andalso Local_Theory.level lthy = 1
-      then error "Not possible on level of global theory" else ();
+    val _ = assert_not_theory lthy;
   in
     lthy
-    |> Local_Theory.mark_brittle
     |> generic_interpretation cert_goal_expression (K I) (K I) Element.witness_proof_eqs
-        Local_Theory.notes_kind activate_local_theory expression raw_eqns
+        Local_Theory.notes_kind Local_Theory.activate expression raw_eqns
   end;
 
 fun interpret x = gen_interpret cert_goal_expression (K I) (K I) x;
diff -r 9943f8067f11 -r 893b15200ec1 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Sat May 25 17:40:44 2013 +0200
+++ b/src/Pure/Isar/local_theory.ML	Sat May 25 18:30:38 2013 +0200
@@ -14,7 +14,6 @@
   val restore: local_theory -> local_theory
   val level: Proof.context -> int
   val assert_bottom: bool -> local_theory -> local_theory
-  val mark_brittle: local_theory -> local_theory
   val assert_nonbrittle: local_theory -> local_theory
   val open_target: Name_Space.naming -> operations -> (local_theory -> local_theory) ->
     local_theory -> local_theory
@@ -36,7 +35,6 @@
   val target_of: local_theory -> Proof.context
   val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
   val target_morphism: local_theory -> morphism
-  val surface_target: (Proof.context -> Proof.context) -> local_theory -> local_theory
   val propagate_ml_env: generic_theory -> generic_theory
   val operations_of: local_theory -> operations
   val define: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
@@ -58,6 +56,12 @@
   val class_alias: binding -> class -> local_theory -> local_theory
   val type_alias: binding -> string -> local_theory -> local_theory
   val const_alias: binding -> string -> local_theory -> local_theory
+  val activate: string * morphism -> (morphism * bool) option -> morphism ->
+    local_theory -> local_theory
+  val add_registration: string * morphism -> (morphism * bool) option -> morphism ->
+    local_theory -> local_theory
+  val add_dependency: string -> string * morphism -> (morphism * bool) option -> morphism ->
+    local_theory -> local_theory
   val init: Name_Space.naming -> operations -> Proof.context -> local_theory
   val exit: local_theory -> Proof.context
   val exit_global: local_theory -> theory
@@ -232,10 +236,6 @@
 
 fun target_morphism lthy = standard_morphism lthy (target_of lthy);
 
-fun surface_target f =
-  map_first_lthy (fn (naming, operations, after_close, brittle, target) =>
-    (naming, operations, after_close, brittle, f target));
-
 fun propagate_ml_env (context as Context.Proof lthy) =
       let val inherit = ML_Env.inherit context in
         lthy
@@ -306,6 +306,22 @@
 val const_alias = alias Sign.const_alias Proof_Context.const_alias;
 
 
+(* activation of locale fragments *)
+
+fun activate_surface dep_morph mixin export =
+  map_first_lthy (fn (naming, operations, after_close, brittle, target) =>
+    (naming, operations, after_close, brittle,
+      (Context.proof_map ooo Locale.add_registration) dep_morph mixin export target));
+
+fun activate dep_morph mixin export =
+  mark_brittle #> activate_surface dep_morph mixin export;
+
+val add_registration = raw_theory o Context.theory_map ooo Locale.add_registration;
+
+fun add_dependency locale dep_morph mixin export =
+  (raw_theory ooo Locale.add_dependency locale) dep_morph mixin export
+  #> activate_surface dep_morph mixin export;
+
 
 (** init and exit **)
 
diff -r 9943f8067f11 -r 893b15200ec1 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Sat May 25 17:40:44 2013 +0200
+++ b/src/Pure/Isar/named_target.ML	Sat May 25 18:30:38 2013 +0200
@@ -8,6 +8,8 @@
 signature NAMED_TARGET =
 sig
   val peek: local_theory -> {target: string, is_locale: bool, is_class: bool} option
+  val is_theory: local_theory -> bool
+  val the_name: local_theory -> string
   val init: (local_theory -> local_theory) -> string -> theory -> local_theory
   val theory_init: theory -> local_theory
   val reinit: local_theory -> local_theory -> local_theory
@@ -43,6 +45,17 @@
   Data.get #> Option.map (fn Target {target, is_locale, is_class, ...} =>
     {target = target, is_locale = is_locale, is_class = is_class});
 
+fun is_theory lthy = Option.map #target (peek lthy) = SOME ""
+  andalso Local_Theory.level lthy = 1;
+
+fun the_name lthy =
+  let
+    val _ = Local_Theory.assert_bottom true lthy;
+  in case Option.map #target (peek lthy) of
+      SOME target => target
+    | _ => error "Not in a named target"
+  end;
+
 
 (* consts in locale *)
 
diff -r 9943f8067f11 -r 893b15200ec1 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sat May 25 17:40:44 2013 +0200
+++ b/src/Pure/ROOT.ML	Sat May 25 18:30:38 2013 +0200
@@ -230,8 +230,8 @@
 use "Isar/obtain.ML";
 
 (*local theories and targets*)
+use "Isar/locale.ML";
 use "Isar/local_theory.ML";
-use "Isar/locale.ML";
 use "Isar/generic_target.ML";
 use "Isar/overloading.ML";
 use "axclass.ML";