src/HOL/MicroJava/DFA/Kildall.thy
changeset 41413 64cd30d6b0b8
parent 35416 d8d7d1b785af
child 41541 1fa4725c4656
     1.1 --- a/src/HOL/MicroJava/DFA/Kildall.thy	Wed Dec 29 13:51:17 2010 +0100
     1.2 +++ b/src/HOL/MicroJava/DFA/Kildall.thy	Wed Dec 29 17:34:41 2010 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* \isaheader{Kildall's Algorithm}\label{sec:Kildall} *}
     1.5  
     1.6  theory Kildall
     1.7 -imports SemilatAlg While_Combinator
     1.8 +imports SemilatAlg "~~/src/HOL/Library/While_Combinator"
     1.9  begin
    1.10  
    1.11  primrec propa :: "'s binop \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's list \<Rightarrow> nat set \<Rightarrow> 's list * nat set" where