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