equal
deleted
inserted
replaced
6 Kildall's algorithm |
6 Kildall's algorithm |
7 *) |
7 *) |
8 |
8 |
9 header {* \isaheader{Kildall's Algorithm}\label{sec:Kildall} *} |
9 header {* \isaheader{Kildall's Algorithm}\label{sec:Kildall} *} |
10 |
10 |
11 theory Kildall = SemilatAlg + While_Combinator: |
11 theory Kildall imports SemilatAlg While_Combinator begin |
12 |
12 |
13 |
13 |
14 consts |
14 consts |
15 iter :: "'s binop \<Rightarrow> 's step_type \<Rightarrow> |
15 iter :: "'s binop \<Rightarrow> 's step_type \<Rightarrow> |
16 's list \<Rightarrow> nat set \<Rightarrow> 's list \<times> nat set" |
16 's list \<Rightarrow> nat set \<Rightarrow> 's list \<times> nat set" |