src/HOL/Analysis/Polytope.thy
changeset 67831 07f5588f2735
parent 67829 2a6ef5ba4822
child 67968 a5ad4c015d1c
     1.1 --- a/src/HOL/Analysis/Polytope.thy	Mon Mar 12 20:53:29 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Polytope.thy	Mon Mar 12 21:03:57 2018 +0100
     1.3 @@ -735,11 +735,7 @@
     1.4    show ?thesis
     1.5    proof (cases "Q = {}")
     1.6      case True then show ?thesis
     1.7 -      sledgehammer
     1.8        by (metis IntQ Inter_UNIV_conv(2) assms(1) assms(2) ex_in_conv)
     1.9 -(*
    1.10 -      by (metis Inf_empty Inf_lower IntQ assms ex_in_conv subset_antisym top_greatest)
    1.11 -*)
    1.12    next
    1.13      case False
    1.14      have "Q \<subseteq> {T. T exposed_face_of S}"