# HG changeset patch
# User haftmann
# Date 1491982067 -7200
# Node ID b0f89998c2a135d1d1af669d1e1917e26a6766fe
# Parent  067210a08a220f66230a0894038d19aee2a5f4e2
tuned

diff -r 067210a08a22 -r b0f89998c2a1 src/HOL/Conditionally_Complete_Lattices.thy
--- a/src/HOL/Conditionally_Complete_Lattices.thy	Wed Apr 12 09:27:43 2017 +0200
+++ b/src/HOL/Conditionally_Complete_Lattices.thy	Wed Apr 12 09:27:47 2017 +0200
@@ -10,12 +10,19 @@
 imports Finite_Set Lattices_Big Set_Interval
 begin
 
-lemma (in linorder) Sup_fin_eq_Max: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup_fin X = Max X"
+context linorder
+begin
+  
+lemma Sup_fin_eq_Max:
+  "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup_fin X = Max X"
   by (induct X rule: finite_ne_induct) (simp_all add: sup_max)
 
-lemma (in linorder) Inf_fin_eq_Min: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf_fin X = Min X"
+lemma Inf_fin_eq_Min:
+  "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf_fin X = Min X"
   by (induct X rule: finite_ne_induct) (simp_all add: inf_min)
 
+end
+
 context preorder
 begin
 
diff -r 067210a08a22 -r b0f89998c2a1 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Wed Apr 12 09:27:43 2017 +0200
+++ b/src/HOL/Library/Multiset.thy	Wed Apr 12 09:27:47 2017 +0200
@@ -503,10 +503,10 @@
 subsubsection \<open>Pointwise ordering induced by count\<close>
 
 definition subseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<subseteq>#" 50)
-  where "A \<subseteq># B = (\<forall>a. count A a \<le> count B a)"
+  where "A \<subseteq># B \<longleftrightarrow> (\<forall>a. count A a \<le> count B a)"
 
 definition subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<subset>#" 50)
-  where "A \<subset># B = (A \<subseteq># B \<and> A \<noteq> B)"
+  where "A \<subset># B \<longleftrightarrow> A \<subseteq># B \<and> A \<noteq> B"
 
 abbreviation (input) supseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<supseteq>#" 50)
   where "supseteq_mset A B \<equiv> B \<subseteq># A"