# HG changeset patch
# User Manuel Eberl <eberlm@in.tum.de>
# Date 1520885037 -3600
# Node ID 07f5588f2735c6dd8b39927840744cfbb3fa6a2a
# Parent  4f992daf47078dedaa2690bbb81a52f97ef0bc57
Removed stray 'sledgehammer' invocation

diff -r 4f992daf4707 -r 07f5588f2735 CONTRIBUTORS
--- 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
 
diff -r 4f992daf4707 -r 07f5588f2735 NEWS
--- 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
diff -r 4f992daf4707 -r 07f5588f2735 src/HOL/Analysis/Polytope.thy
--- 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}"