src/HOL/Analysis/Tagged_Division.thy
changeset 68120 2f161c6910f7
parent 67968 a5ad4c015d1c
child 68302 b6567edf3b3d
     1.1 --- a/src/HOL/Analysis/Tagged_Division.thy	Sun May 06 23:59:14 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Tagged_Division.thy	Tue May 08 10:32:07 2018 +0100
     1.3 @@ -685,7 +685,7 @@
     1.4  
     1.5  lemma elementary_subset_cbox:
     1.6    "p division_of S \<Longrightarrow> \<exists>a b. S \<subseteq> cbox a (b::'a::euclidean_space)"
     1.7 -  by (meson elementary_bounded bounded_subset_cbox)
     1.8 +  by (meson bounded_subset_cbox_symmetric elementary_bounded)
     1.9  
    1.10  lemma division_union_intervals_exists:
    1.11    fixes a b :: "'a::euclidean_space"