src/HOL/IMP/Abs_Int1_ivl.thy
changeset 45990 b7b905b23b2a
parent 45978 d3325de5f299
child 46028 9f113cdf3d66
     1.1 --- a/src/HOL/IMP/Abs_Int1_ivl.thy	Mon Dec 26 22:17:10 2011 +0100
     1.2 +++ b/src/HOL/IMP/Abs_Int1_ivl.thy	Mon Dec 26 22:17:10 2011 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4  (* Author: Tobias Nipkow *)
     1.5  
     1.6  theory Abs_Int1_ivl
     1.7 -imports Abs_Int1 Abs_Int_Tests "~~/src/HOL/Library/More_Set"
     1.8 +imports Abs_Int1 Abs_Int_Tests
     1.9  begin
    1.10  
    1.11  subsection "Interval Analysis"