src/HOL/Library/Convex.thy
changeset 60303 00c06f1315d0
parent 60178 f620c70f9e9b
child 60423 5035a2af185b
     1.1 --- a/src/HOL/Library/Convex.thy	Mon May 25 22:52:17 2015 +0200
     1.2 +++ b/src/HOL/Library/Convex.thy	Tue May 26 21:58:04 2015 +0100
     1.3 @@ -48,13 +48,13 @@
     1.4    shows "((1 - u) *\<^sub>R a + u *\<^sub>R b) \<in> s"
     1.5    using assms unfolding convex_alt by auto
     1.6  
     1.7 -lemma convex_empty[intro]: "convex {}"
     1.8 +lemma convex_empty[intro,simp]: "convex {}"
     1.9    unfolding convex_def by simp
    1.10  
    1.11 -lemma convex_singleton[intro]: "convex {a}"
    1.12 +lemma convex_singleton[intro,simp]: "convex {a}"
    1.13    unfolding convex_def by (auto simp: scaleR_left_distrib[symmetric])
    1.14  
    1.15 -lemma convex_UNIV[intro]: "convex UNIV"
    1.16 +lemma convex_UNIV[intro,simp]: "convex UNIV"
    1.17    unfolding convex_def by auto
    1.18  
    1.19  lemma convex_Inter: "(\<forall>s\<in>f. convex s) \<Longrightarrow> convex(\<Inter> f)"