src/HOL/MicroJava/BV/DFA_Framework.thy

--- a/src/HOL/MicroJava/BV/DFA_Framework.thy	Tue Dec 05 14:08:22 2000 +0100
+++ b/src/HOL/MicroJava/BV/DFA_Framework.thy	Tue Dec 05 14:08:56 2000 +0100
@@ -11,6 +11,8 @@
 theory DFA_Framework = Listn:
 
 constdefs
+ bounded :: "(nat => nat list) => nat => bool"
+"bounded succs n == !p<n. !q:set(succs p). q<n"
 
  stable :: "'s ord =>
            (nat => 's => 's)