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

Mon Mar 12 21:03:57 2018 +0100 (22 months ago ago) | |

changeset 67831 | 07f5588f2735 |

parent 67830 | 4f992daf4707 |

child 67849 | d4c8b2cf685f |

Removed stray 'sledgehammer' invocation

CONTRIBUTORS | file | annotate | diff | revisions | |

NEWS | file | annotate | diff | revisions | |

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

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