summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | Manuel Eberl <eberlm@in.tum.de> |

Mon, 12 Mar 2018 21:03:57 +0100 | |

changeset 67831 | 07f5588f2735 |

parent 67830 | 4f992daf4707 |

child 67849 | d4c8b2cf685f |

Removed stray 'sledgehammer' invocation

CONTRIBUTORS | file | annotate | diff | comparison | revisions | |

NEWS | file | annotate | diff | comparison | revisions | |

src/HOL/Analysis/Polytope.thy | file | annotate | diff | comparison | revisions |

--- 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}"