changeset 46861 | b7b905b23b2a |
parent 46849 | d3325de5f299 |
child 46899 | 9f113cdf3d66 |
46860:b39256df5f8a | 46861:b7b905b23b2a |
---|---|
1 (* Author: Tobias Nipkow *) |
1 (* Author: Tobias Nipkow *) |
2 |
2 |
3 theory Abs_Int_den1_ivl |
3 theory Abs_Int_den1_ivl |
4 imports Abs_Int_den1 "~~/src/HOL/Library/More_Set" |
4 imports Abs_Int_den1 |
5 begin |
5 begin |
6 |
6 |
7 subsection "Interval Analysis" |
7 subsection "Interval Analysis" |
8 |
8 |
9 datatype ivl = I "int option" "int option" |
9 datatype ivl = I "int option" "int option" |