1.1 --- a/src/HOL/IMP/Abs_Int2_ivl.thy	Thu May 02 21:04:50 2013 +0200
     1.2 +++ b/src/HOL/IMP/Abs_Int2_ivl.thy	Fri May 03 02:52:25 2013 +0200
     1.3 @@ -186,6 +186,9 @@
     1.4  lemma inf_ivl_nice: "[l1\<dots>h1] \<sqinter> [l2\<dots>h2] = [max l1 l2\<dots>min h1 h2]"
     1.5  by transfer (simp add: inf_rep_def)
     1.6  
     1.7 +lemma top_ivl_nice: "\<top> = [-\<infinity>\<dots>\<infinity>]"
     1.8 +by (simp add: top_ivl_def)
     1.9 +
    1.10  
    1.11  instantiation ivl :: plus
    1.12  begin