# HG changeset patch
# User wenzelm
# Date 1517256882 -3600
# Node ID ea029c521b5bf395f85f6df589efdfb69c24d43f
# Parent  a585c5b53576a4f6ad57808c89887de71b654e32# Parent  a93a9e89da7244232dbab26ab220edab1a202c16
merged

diff -r a93a9e89da72 -r ea029c521b5b NEWS
--- a/NEWS	Mon Jan 29 20:37:28 2018 +0100
+++ b/NEWS	Mon Jan 29 21:14:42 2018 +0100
@@ -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 a93a9e89da72 -r ea029c521b5b src/Doc/Codegen/Computations.thy
--- a/src/Doc/Codegen/Computations.thy	Mon Jan 29 20:37:28 2018 +0100
+++ b/src/Doc/Codegen/Computations.thy	Mon Jan 29 21:14:42 2018 +0100
@@ -1,7 +1,6 @@
 theory Computations
   imports Codegen_Basics.Setup
     "HOL-Library.Code_Target_Int"
-    "HOL-Library.Code_Char"
 begin
 
 section \<open>Computations \label{sec:computations}\<close>
diff -r a93a9e89da72 -r ea029c521b5b src/HOL/Lattices_Big.thy
--- a/src/HOL/Lattices_Big.thy	Mon Jan 29 20:37:28 2018 +0100
+++ b/src/HOL/Lattices_Big.thy	Mon Jan 29 21:14:42 2018 +0100
@@ -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