diff -r b732997cfc11 -r 42d11e0a7a8b src/HOL/MicroJava/BV/StepMono.thy
--- a/src/HOL/MicroJava/BV/StepMono.thy	Mon Aug 14 14:57:29 2000 +0200
+++ b/src/HOL/MicroJava/BV/StepMono.thy	Mon Aug 14 18:03:19 2000 +0200
@@ -4,34 +4,13 @@
     Copyright   2000 Technische Universitaet Muenchen
 *)
 
-header {* Monotonicity of \texttt{step} and \texttt{app} *}
-
-theory StepMono = Step :
-
+header {* Monotonicity of step and app *}
 
-lemmas [trans] = sup_state_trans sup_loc_trans widen_trans
-
+theory StepMono = Step:
 
-lemma sup_state_length:
-"G \<turnstile> s2 <=s s1 \<Longrightarrow> length (fst s2) = length (fst s1) \<and> length (snd s2) = length (snd s1)"
-  by (cases s1, cases s2, simp add: sup_state_length_fst sup_state_length_snd)
-  
 
 lemma PrimT_PrimT: "(G \<turnstile> xb \<preceq> PrimT p) = (xb = PrimT p)"
-proof
-  show "xb = PrimT p \<Longrightarrow> G \<turnstile> xb \<preceq> PrimT p" by blast
-
-  show "G\<turnstile> xb \<preceq> PrimT p \<Longrightarrow> xb = PrimT p"
-  proof (cases xb)
-    fix prim
-    assume "xb = PrimT prim" "G\<turnstile>xb\<preceq>PrimT p"
-    thus ?thesis by simp
-  next
-    fix ref
-    assume "G\<turnstile>xb\<preceq>PrimT p" "xb = RefT ref"
-    thus ?thesis by simp (rule widen_RefT [elimify], auto)
-  qed
-qed
+  by (auto elim: widen.elims)
 
 
 lemma sup_loc_some [rulify]:
@@ -50,7 +29,7 @@
     show "(\<exists>t. (a # list) ! n = Some t) \<and> G \<turnstile>(a # list) ! n <=o Some t" 
     proof (cases n) 
       case 0
-      with * show ?thesis by (simp add: sup_ty_opt_some)
+      with * show ?thesis by (simp add: sup_ty_opt_Some)
     next
       case Suc
       with Cons *
@@ -159,7 +138,7 @@
     with G app
     show ?thesis
       by - (cases s2,
-            auto dest: map_hd_tl simp add: sup_loc_Cons2 sup_loc_length sup_state_def)
+            auto simp add: map_eq_Cons sup_loc_Cons2 sup_loc_length sup_state_def)
   next
     case Bipush
     thus ?thesis by simp