equal
deleted
inserted
replaced
1 (* Author: Tobias Nipkow *) |
1 (* Author: Tobias Nipkow *) |
|
2 |
|
3 subsection "Interval Analysis" |
2 |
4 |
3 theory Abs_Int2_ivl |
5 theory Abs_Int2_ivl |
4 imports Abs_Int2 |
6 imports Abs_Int2 |
5 begin |
7 begin |
6 |
|
7 subsection "Interval Analysis" |
|
8 |
8 |
9 type_synonym eint = "int extended" |
9 type_synonym eint = "int extended" |
10 type_synonym eint2 = "eint * eint" |
10 type_synonym eint2 = "eint * eint" |
11 |
11 |
12 definition \<gamma>_rep :: "eint2 \<Rightarrow> int set" where |
12 definition \<gamma>_rep :: "eint2 \<Rightarrow> int set" where |