diff -r 75b2edff1af3 -r 4b1edf2f6bd2 src/HOL/MicroJava/BV/Typing_Framework.thy
--- a/src/HOL/MicroJava/BV/Typing_Framework.thy	Mon Mar 18 11:47:03 2002 +0100
+++ b/src/HOL/MicroJava/BV/Typing_Framework.thy	Wed Mar 20 13:21:07 2002 +0100
@@ -15,9 +15,6 @@
   's step_type = "nat \<Rightarrow> 's \<Rightarrow> (nat \<times> 's) list"
 
 constdefs
- bounded :: "'s step_type \<Rightarrow> nat \<Rightarrow> bool"
-"bounded step n == !p<n. !s. !(q,t):set(step p s). q<n"  
-
  stable :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> nat \<Rightarrow> bool"
 "stable r step ss p == !(q,s'):set(step p (ss!p)). s' <=_r ss!q"