equal
deleted
inserted
replaced
3 theory Abs_Int2_ivl |
3 theory Abs_Int2_ivl |
4 imports Abs_Int2 |
4 imports Abs_Int2 |
5 begin |
5 begin |
6 |
6 |
7 subsection "Interval Analysis" |
7 subsection "Interval Analysis" |
8 |
|
9 text{* Drop @{const Fin} around numerals on output from value command: *} |
|
10 declare Fin_numeral[code_post] Fin_neg_numeral[code_post] |
|
11 zero_extended_def[symmetric, code_post] one_extended_def[symmetric, code_post] |
|
12 |
8 |
13 type_synonym eint = "int extended" |
9 type_synonym eint = "int extended" |
14 type_synonym eint2 = "eint * eint" |
10 type_synonym eint2 = "eint * eint" |
15 |
11 |
16 definition \<gamma>_rep :: "eint2 \<Rightarrow> int set" where |
12 definition \<gamma>_rep :: "eint2 \<Rightarrow> int set" where |