| changeset 66453 | cc19f7ca2ed6 |
| parent 62042 | 6c6ccf573479 |
| child 67443 | 3abf6a722518 |
--- a/src/HOL/MicroJava/DFA/Kildall.thy Fri Aug 18 13:55:05 2017 +0200 +++ b/src/HOL/MicroJava/DFA/Kildall.thy Fri Aug 18 20:47:47 2017 +0200 @@ -6,7 +6,7 @@ section \<open>Kildall's Algorithm \label{sec:Kildall}\<close> theory Kildall -imports SemilatAlg "~~/src/HOL/Library/While_Combinator" +imports SemilatAlg "HOL-Library.While_Combinator" begin primrec propa :: "'s binop \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's list \<Rightarrow> nat set \<Rightarrow> 's list * nat set" where