src/HOL/MicroJava/BV/DFA_err.thy

--- a/src/HOL/MicroJava/BV/DFA_err.thy	Tue Dec 05 14:08:22 2000 +0100
+++ b/src/HOL/MicroJava/BV/DFA_err.thy	Tue Dec 05 14:08:56 2000 +0100
@@ -25,9 +25,6 @@
              (nat => 's err => 's err)"
 "err_step app step p == lift (%t. if app p t then OK (step p t) else Err)"
 
-bounded :: "(nat => nat list) => nat => bool"
-"bounded succs n == !p<n. !q:set(succs p). q<n"
-
 non_empty :: "(nat => nat list) => bool"
 "non_empty succs == !p. succs p ~= []"