equal
deleted
inserted
replaced
4 imports AbsInt1_ivl |
4 imports AbsInt1_ivl |
5 begin |
5 begin |
6 |
6 |
7 subsection "Widening and Narrowing" |
7 subsection "Widening and Narrowing" |
8 |
8 |
9 text{* The assumptions about winden and narrow are merely sanity checks. They |
9 text{* The assumptions about widen and narrow are merely sanity checks. They |
10 are only needed in case we want to prove termination of the fixedpoint |
10 are only needed in case we want to prove termination of the fixedpoint |
11 iteration, which we do not --- we limit the number of iterations as before. *} |
11 iteration, which we do not --- we limit the number of iterations as before. *} |
12 |
12 |
13 class WN = SL_top + |
13 class WN = SL_top + |
14 fixes widen :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<nabla>" 65) |
14 fixes widen :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<nabla>" 65) |