equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 header {* \isaheader{Kildall's Algorithm}\label{sec:Kildall} *} |
6 header {* \isaheader{Kildall's Algorithm}\label{sec:Kildall} *} |
7 |
7 |
8 theory Kildall |
8 theory Kildall |
9 imports SemilatAlg While_Combinator |
9 imports SemilatAlg "~~/src/HOL/Library/While_Combinator" |
10 begin |
10 begin |
11 |
11 |
12 primrec propa :: "'s binop \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's list \<Rightarrow> nat set \<Rightarrow> 's list * nat set" where |
12 primrec propa :: "'s binop \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's list \<Rightarrow> nat set \<Rightarrow> 's list * nat set" where |
13 "propa f [] ss w = (ss,w)" |
13 "propa f [] ss w = (ss,w)" |
14 | "propa f (q'#qs) ss w = (let (q,t) = q'; |
14 | "propa f (q'#qs) ss w = (let (q,t) = q'; |