--- a/src/HOL/MicroJava/BV/StepMono.thy Sun Jan 14 18:17:37 2001 +0100
+++ b/src/HOL/MicroJava/BV/StepMono.thy Sun Jan 14 18:19:18 2001 +0100
@@ -143,11 +143,7 @@
by - (cases s2, auto simp add: map_eq_Cons sup_loc_Cons2
sup_loc_length sup_state_conv)
next
- case Bipush
- with G app
- show ?thesis by simp
- next
- case Aconst_null
+ case LitPush
with G app
show ?thesis by simp
next
@@ -355,7 +351,7 @@
show ?thesis
by (clarsimp simp add: sup_state_conv sup_loc_update)
next
- case Bipush
+ case LitPush
with G s step app1 app2
show ?thesis
by (clarsimp simp add: sup_state_Cons1)
@@ -365,11 +361,6 @@
show ?thesis
by (clarsimp simp add: sup_state_Cons1)
next
- case Aconst_null
- with G s step app1 app2
- show ?thesis
- by (clarsimp simp add: sup_state_Cons1)
- next
case Getfield
with G s step app1 app2
show ?thesis