--- a/CONTRIBUTORS Mon Mar 12 20:53:29 2018 +0100
+++ b/CONTRIBUTORS Mon Mar 12 21:03:57 2018 +0100
@@ -6,6 +6,9 @@
Contributions to this Isabelle version
--------------------------------------
+* March 2018: Viorel Preoteasa
+ Generalisation of complete_distrib_lattice
+
* January 2018: Sebastien Gouezel
Various small additions to HOL-Analysis
--- a/NEWS Mon Mar 12 20:53:29 2018 +0100
+++ b/NEWS Mon Mar 12 21:03:57 2018 +0100
@@ -9,16 +9,6 @@
*** General ***
-* New, more general, axiomatization of complete_distrib_lattice.
-The former axioms:
-"sup x (Inf X) = Inf (sup x ` X)" and "inf x (Sup X) = Sup (inf x ` X)"
-are replaced by
-"Inf (Sup ` A) <= Sup (Inf ` {f ` A | f . (! Y \<in> A . f Y \<in> Y)})"
-The instantiations of sets and functions as complete_distrib_lattice
-are moved to Hilbert_Choice.thy because their proofs need the Hilbert
-choice operator. The dual of this property is also proved in
-Hilbert_Choice.thy.
-
* Marginal comments need to be written exclusively in the new-style form
"\<comment> \<open>text\<close>", old ASCII variants like "-- {* ... *}" are no longer
supported. INCOMPATIBILITY, use the command-line tool "isabelle
@@ -204,6 +194,16 @@
*** HOL ***
+* New, more general, axiomatization of complete_distrib_lattice.
+The former axioms:
+"sup x (Inf X) = Inf (sup x ` X)" and "inf x (Sup X) = Sup (inf x ` X)"
+are replaced by
+"Inf (Sup ` A) <= Sup (Inf ` {f ` A | f . (! Y \<in> A . f Y \<in> Y)})"
+The instantiations of sets and functions as complete_distrib_lattice
+are moved to Hilbert_Choice.thy because their proofs need the Hilbert
+choice operator. The dual of this property is also proved in
+Hilbert_Choice.thy.
+
* Clarifed theorem names:
Min.antimono ~> Min.subset_imp
--- a/src/HOL/Analysis/Polytope.thy Mon Mar 12 20:53:29 2018 +0100
+++ b/src/HOL/Analysis/Polytope.thy Mon Mar 12 21:03:57 2018 +0100
@@ -735,11 +735,7 @@
show ?thesis
proof (cases "Q = {}")
case True then show ?thesis
- sledgehammer
by (metis IntQ Inter_UNIV_conv(2) assms(1) assms(2) ex_in_conv)
-(*
- by (metis Inf_empty Inf_lower IntQ assms ex_in_conv subset_antisym top_greatest)
-*)
next
case False
have "Q \<subseteq> {T. T exposed_face_of S}"