src/HOL/Analysis/Ordered_Euclidean_Space.thy
changeset 68120 2f161c6910f7
parent 67981 349c639e593c
child 68239 0764ee22a4d1
     1.1 --- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Sun May 06 23:59:14 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Tue May 08 10:32:07 2018 +0100
     1.3 @@ -267,7 +267,7 @@
     1.4      and bdd_below_box[intro, simp]: "bdd_below (box a b)"
     1.5    unfolding atomize_conj
     1.6    by (metis bdd_above_Icc bdd_above_mono bdd_below_Icc bdd_below_mono bounded_box
     1.7 -    bounded_subset_cbox interval_cbox)
     1.8 +            bounded_subset_cbox_symmetric interval_cbox)
     1.9  
    1.10  instantiation vec :: (ordered_euclidean_space, finite) ordered_euclidean_space
    1.11  begin