Removed stray 'sledgehammer' invocation
authorManuel Eberl <eberlm@in.tum.de>
Mon Mar 12 21:03:57 2018 +0100 (15 months ago)
changeset 6783107f5588f2735
parent 67830 4f992daf4707
child 67849 d4c8b2cf685f
Removed stray 'sledgehammer' invocation
CONTRIBUTORS
NEWS
src/HOL/Analysis/Polytope.thy
     1.1 --- a/CONTRIBUTORS	Mon Mar 12 20:53:29 2018 +0100
     1.2 +++ b/CONTRIBUTORS	Mon Mar 12 21:03:57 2018 +0100
     1.3 @@ -6,6 +6,9 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 +* March 2018: Viorel Preoteasa
     1.8 +  Generalisation of complete_distrib_lattice
     1.9 +
    1.10  * January 2018: Sebastien Gouezel
    1.11    Various small additions to HOL-Analysis
    1.12  
     2.1 --- a/NEWS	Mon Mar 12 20:53:29 2018 +0100
     2.2 +++ b/NEWS	Mon Mar 12 21:03:57 2018 +0100
     2.3 @@ -9,16 +9,6 @@
     2.4  
     2.5  *** General ***
     2.6  
     2.7 -* New, more general, axiomatization of complete_distrib_lattice. 
     2.8 -The former axioms:
     2.9 -"sup x (Inf X) = Inf (sup x ` X)" and "inf x (Sup X) = Sup (inf x ` X)"
    2.10 -are replaced by 
    2.11 -"Inf (Sup ` A) <= Sup (Inf ` {f ` A | f . (! Y \<in> A . f Y \<in> Y)})"
    2.12 -The instantiations of sets and functions as complete_distrib_lattice 
    2.13 -are moved to Hilbert_Choice.thy because their proofs need the Hilbert
    2.14 -choice operator. The dual of this property is also proved in 
    2.15 -Hilbert_Choice.thy.
    2.16 -
    2.17  * Marginal comments need to be written exclusively in the new-style form
    2.18  "\<comment> \<open>text\<close>", old ASCII variants like "-- {* ... *}" are no longer
    2.19  supported. INCOMPATIBILITY, use the command-line tool "isabelle
    2.20 @@ -204,6 +194,16 @@
    2.21  
    2.22  *** HOL ***
    2.23  
    2.24 +* New, more general, axiomatization of complete_distrib_lattice. 
    2.25 +The former axioms:
    2.26 +"sup x (Inf X) = Inf (sup x ` X)" and "inf x (Sup X) = Sup (inf x ` X)"
    2.27 +are replaced by 
    2.28 +"Inf (Sup ` A) <= Sup (Inf ` {f ` A | f . (! Y \<in> A . f Y \<in> Y)})"
    2.29 +The instantiations of sets and functions as complete_distrib_lattice 
    2.30 +are moved to Hilbert_Choice.thy because their proofs need the Hilbert
    2.31 +choice operator. The dual of this property is also proved in 
    2.32 +Hilbert_Choice.thy.
    2.33 +
    2.34  * Clarifed theorem names:
    2.35  
    2.36    Min.antimono ~> Min.subset_imp
     3.1 --- a/src/HOL/Analysis/Polytope.thy	Mon Mar 12 20:53:29 2018 +0100
     3.2 +++ b/src/HOL/Analysis/Polytope.thy	Mon Mar 12 21:03:57 2018 +0100
     3.3 @@ -735,11 +735,7 @@
     3.4    show ?thesis
     3.5    proof (cases "Q = {}")
     3.6      case True then show ?thesis
     3.7 -      sledgehammer
     3.8        by (metis IntQ Inter_UNIV_conv(2) assms(1) assms(2) ex_in_conv)
     3.9 -(*
    3.10 -      by (metis Inf_empty Inf_lower IntQ assms ex_in_conv subset_antisym top_greatest)
    3.11 -*)
    3.12    next
    3.13      case False
    3.14      have "Q \<subseteq> {T. T exposed_face_of S}"