--- a/NEWS Mon Jan 29 19:26:14 2018 +0100
+++ b/NEWS Sun Jan 28 16:38:48 2018 +0000
@@ -169,6 +169,13 @@
*** HOL ***
+* Clarifed theorem names:
+
+ Min.antimono ~> Min.subset_imp
+ Max.antimono ~> Max.subset_imp
+
+Minor INCOMPATIBILITY.
+
* A new command parametric_constant for proving parametricity of
non-recursive definitions. For constants that are not fully parametric
the command will infer conditions on relations (e.g., bi_unique,
--- a/src/HOL/Lattices_Big.thy Mon Jan 29 19:26:14 2018 +0100
+++ b/src/HOL/Lattices_Big.thy Sun Jan 28 16:38:48 2018 +0000
@@ -132,7 +132,7 @@
lemma bounded_iff:
assumes "finite A" and "A \<noteq> {}"
shows "x \<^bold>\<le> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<^bold>\<le> a)"
- using assms by (induct rule: finite_ne_induct) (simp_all add: bounded_iff)
+ using assms by (induct rule: finite_ne_induct) simp_all
lemma boundedI:
assumes "finite A"
@@ -162,7 +162,7 @@
qed
qed
-lemma antimono:
+lemma subset_imp:
assumes "A \<subseteq> B" and "A \<noteq> {}" and "finite B"
shows "F B \<^bold>\<le> F A"
proof (cases "A = B")
@@ -256,7 +256,7 @@
lemma bounded_iff:
assumes "finite A"
shows "x \<^bold>\<le> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<^bold>\<le> a)"
- using assms by (induct A) (simp_all add: bounded_iff)
+ using assms by (induct A) simp_all
lemma boundedI:
assumes "finite A"
@@ -285,7 +285,7 @@
qed
qed
-lemma antimono:
+lemma subset_imp:
assumes "A \<subseteq> B" and "finite B"
shows "F B \<^bold>\<le> F A"
proof (cases "A = B")
@@ -648,12 +648,12 @@
lemma Min_antimono:
assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
shows "Min N \<le> Min M"
- using assms by (fact Min.antimono)
+ using assms by (fact Min.subset_imp)
lemma Max_mono:
assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
shows "Max M \<le> Max N"
- using assms by (fact Max.antimono)
+ using assms by (fact Max.subset_imp)
end