| changeset 10592 | fc0b575a2cf7 |
| parent 10496 | f2d304bdf3cc |
| child 10661 | fcd8d4e7d758 |
--- a/src/HOL/MicroJava/BV/Kildall.thy Tue Dec 05 14:08:22 2000 +0100 +++ b/src/HOL/MicroJava/BV/Kildall.thy Tue Dec 05 14:08:56 2000 +0100 @@ -11,9 +11,6 @@ theory Kildall = DFA_Framework: constdefs - bounded :: "(nat => nat list) => nat => bool" -"bounded succs n == !p<n. !q:set(succs p). q<n" - pres_type :: "(nat => 's => 's) => nat => 's set => bool" "pres_type step n A == !s:A. !p<n. step p s : A"