# HG changeset patch
# User haftmann
# Date 1517157528 0
# Node ID 5d04d7bcd5f66b9e4bc3e09a64f768cf5e802c99
# Parent  a23c3ec2ff28500c0f81d5f759e096c1c84965c1
avoid concrete (anti)mono in theorem names since it could be the other way round

diff -r a23c3ec2ff28 -r 5d04d7bcd5f6 NEWS
--- 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,
diff -r a23c3ec2ff28 -r 5d04d7bcd5f6 src/HOL/Lattices_Big.thy
--- 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