--- 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
--- 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"