# HG changeset patch
# User kleing
# Date 969557157 -7200
# Node ID 9f84ffa4a8d07129bd52186281c0551a6151e9b1
# Parent  2264bdd8becc497f706b21c39d0789f5d4cfc52a
tuned spacing for document generation

diff -r 2264bdd8becc -r 9f84ffa4a8d0 src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Thu Sep 21 18:58:25 2000 +0200
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Thu Sep 21 19:25:57 2000 +0200
@@ -7,11 +7,13 @@
 programs.
 *)
 
-header "Type Safety Proof"
+header "BV Type Safety Proof"
 
 theory BVSpecTypeSafe = Correct:
 
-lemmas defs1 = sup_state_def correct_state_def correct_frame_def wt_instr_def step_def
+lemmas defs1 = sup_state_def correct_state_def correct_frame_def 
+               wt_instr_def step_def
+
 lemmas [simp del] = split_paired_All
 
 lemma wt_jvm_prog_impl_wt_instr_cor:
@@ -25,17 +27,18 @@
 
 lemma Load_correct:
 "[| wf_prog wt G;
-   method (G,C) sig = Some (C,rT,maxl,ins); 
-   ins!pc = Load idx; 
-   wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
-   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); 
-   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
+    method (G,C) sig = Some (C,rT,maxl,ins); 
+    ins!pc = Load idx; 
+    wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
+    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); 
+    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
 ==> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1 map_eq_Cons)
 apply (rule conjI)
  apply (rule approx_loc_imp_approx_val_sup)
  apply simp+
-apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup)
+apply (blast intro: approx_stk_imp_approx_stk_sup 
+                    approx_loc_imp_approx_loc_sup)
 done
 
 lemma Store_correct:
@@ -49,7 +52,8 @@
 apply (clarsimp simp add: defs1 map_eq_Cons)
 apply (rule conjI)
  apply (blast intro: approx_stk_imp_approx_stk_sup)
-apply (blast intro: approx_loc_imp_approx_loc_subst approx_loc_imp_approx_loc_sup)
+apply (blast intro: approx_loc_imp_approx_loc_subst 
+                    approx_loc_imp_approx_loc_sup)
 done
 
 
@@ -60,14 +64,15 @@
 
 lemma Bipush_correct:
 "[| wf_prog wt G;
-  method (G,C) sig = Some (C,rT,maxl,ins); 
-  ins!pc = Bipush i; 
-  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
-  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs);
-  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
+    method (G,C) sig = Some (C,rT,maxl,ins); 
+    ins!pc = Bipush i; 
+    wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
+    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs);
+    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
 ==> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1 approx_val_def sup_PTS_eq map_eq_Cons)
-apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup)
+apply (blast intro: approx_stk_imp_approx_stk_sup 
+                    approx_loc_imp_approx_loc_sup)
 done
 
 lemma NT_subtype_conv:
@@ -87,21 +92,23 @@
 
 lemma Aconst_null_correct:
 "[| wf_prog wt G;
-  method (G,C) sig = Some (C,rT,maxl,ins); 
-  ins!pc =  Aconst_null; 
-  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
-  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); 
-  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
+    method (G,C) sig = Some (C,rT,maxl,ins); 
+    ins!pc =  Aconst_null; 
+    wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
+    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); 
+    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
 ==> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1 map_eq_Cons)
 apply (rule conjI)
  apply (force simp add: approx_val_Null NT_subtype_conv)
-apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup)
+apply (blast intro: approx_stk_imp_approx_stk_sup 
+                    approx_loc_imp_approx_loc_sup)
 done
 
 
 lemma Cast_conf2:
-  "[|wf_prog ok G; G,h\<turnstile>v::\<preceq>RefT rt; cast_ok G C h v; G\<turnstile>Class C\<preceq>T; is_class G C|] 
+  "[| wf_prog ok G; G,h\<turnstile>v::\<preceq>RefT rt; cast_ok G C h v; 
+      G\<turnstile>Class C\<preceq>T; is_class G C|] 
   ==> G,h\<turnstile>v::\<preceq>T"
 apply (unfold cast_ok_def)
 apply (frule widen_Class)
@@ -115,14 +122,15 @@
 
 lemma Checkcast_correct:
 "[| wf_prog wt G;
-  method (G,C) sig = Some (C,rT,maxl,ins); 
-  ins!pc = Checkcast D; 
-  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
-  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
-  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
+    method (G,C) sig = Some (C,rT,maxl,ins); 
+    ins!pc = Checkcast D; 
+    wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
+    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
+    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
 ==> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1 map_eq_Cons raise_xcpt_def approx_val_def)
-apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup Cast_conf2)
+apply (blast intro: approx_stk_imp_approx_stk_sup 
+                    approx_loc_imp_approx_loc_sup Cast_conf2)
 done
 
 
@@ -134,7 +142,8 @@
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
 ==> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs1 raise_xcpt_def map_eq_Cons approx_val_def split: option.split)
+apply (clarsimp simp add: defs1 raise_xcpt_def map_eq_Cons approx_val_def
+                split: option.split)
 apply (frule conf_widen)
 apply assumption+
 apply (drule conf_RefTD)
@@ -143,7 +152,8 @@
  apply (drule widen_cfs_fields)
  apply assumption+
  apply (force intro: conf_widen simp add: hconf_def oconf_def lconf_def)
-apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup)
+apply (blast intro: approx_stk_imp_approx_stk_sup 
+                    approx_loc_imp_approx_loc_sup)
 done
 
 lemma Putfield_correct:
@@ -162,11 +172,14 @@
 apply assumption
 apply (drule conf_RefTD)
 apply clarsimp
-apply (blast intro: sup_heap_update_value approx_stk_imp_approx_stk_sup_heap
-  approx_stk_imp_approx_stk_sup
-  approx_loc_imp_approx_loc_sup_heap approx_loc_imp_approx_loc_sup
-  hconf_imp_hconf_field_update
-  correct_frames_imp_correct_frames_field_update conf_widen dest: widen_cfs_fields)
+apply (blast 
+       intro: 
+         sup_heap_update_value approx_stk_imp_approx_stk_sup_heap
+         approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup_heap 
+         approx_loc_imp_approx_loc_sup hconf_imp_hconf_field_update
+         correct_frames_imp_correct_frames_field_update conf_widen 
+       dest: 
+         widen_cfs_fields)
 done
 
 lemma collapse_paired_All:
@@ -181,15 +194,18 @@
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
 ==> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: NT_subtype_conv approx_val_def conf_def
-		   fun_upd_apply map_eq_Cons is_class_def raise_xcpt_def init_vars_def defs1 
+apply (clarsimp simp add: NT_subtype_conv approx_val_def conf_def defs1
+		   fun_upd_apply map_eq_Cons is_class_def raise_xcpt_def init_vars_def 
        split: option.split)
 apply (force dest!: iffD1 [OF collapse_paired_All]
-            intro: sup_heap_newref approx_stk_imp_approx_stk_sup_heap approx_stk_imp_approx_stk_sup
-                   approx_loc_imp_approx_loc_sup_heap approx_loc_imp_approx_loc_sup
-                   hconf_imp_hconf_newref correct_frames_imp_correct_frames_newref
-                   correct_init_obj simp add:  NT_subtype_conv approx_val_def conf_def
-		   fun_upd_apply map_eq_Cons is_class_def raise_xcpt_def init_vars_def defs1 
+       intro: sup_heap_newref approx_stk_imp_approx_stk_sup_heap 
+              approx_stk_imp_approx_stk_sup 
+              approx_loc_imp_approx_loc_sup_heap 
+              approx_loc_imp_approx_loc_sup
+              hconf_imp_hconf_newref correct_frames_imp_correct_frames_newref
+              correct_init_obj 
+       simp add: NT_subtype_conv approx_val_def conf_def defs1
+         fun_upd_apply map_eq_Cons is_class_def raise_xcpt_def init_vars_def 
        split: option.split)
 done
 
@@ -366,7 +382,8 @@
         by (simp add: wt_start_def sup_state_def)
 
       have r: "approx_loc G hp (replicate mxl' arbitrary) (replicate mxl' Err)"
-        by (simp add: approx_loc_def approx_val_Err list_all2_def set_replicate_conv_if)
+        by (simp add: approx_loc_def approx_val_Err 
+                      list_all2_def set_replicate_conv_if)
 
       from wfprog mD
       have "G \<turnstile> Class D \<preceq> Class D''"
@@ -463,7 +480,8 @@
   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
 ==> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1)
-apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup)
+apply (fast intro: approx_loc_imp_approx_loc_sup 
+                   approx_stk_imp_approx_stk_sup)
 done
 
 
@@ -476,7 +494,8 @@
   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
 ==> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1)
-apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup)
+apply (fast intro: approx_loc_imp_approx_loc_sup 
+                   approx_stk_imp_approx_stk_sup)
 done
 
 lemma Pop_correct:
@@ -488,7 +507,8 @@
   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
 ==> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1)
-apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup)
+apply (fast intro: approx_loc_imp_approx_loc_sup 
+                   approx_stk_imp_approx_stk_sup)
 done
 
 lemma Dup_correct:
@@ -500,7 +520,9 @@
   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
 ==> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1 map_eq_Cons)
-apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
+apply (force intro: approx_stk_imp_approx_stk_sup 
+                    approx_val_imp_approx_val_sup 
+                    approx_loc_imp_approx_loc_sup
              simp add: defs1 map_eq_Cons)
 done
 
@@ -513,7 +535,9 @@
   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
 ==> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1 map_eq_Cons)
-apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
+apply (force intro: approx_stk_imp_approx_stk_sup 
+                    approx_val_imp_approx_val_sup 
+                    approx_loc_imp_approx_loc_sup
              simp add: defs1 map_eq_Cons)
 done
 
@@ -526,7 +550,9 @@
   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
 ==> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1 map_eq_Cons)
-apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
+apply (force intro: approx_stk_imp_approx_stk_sup 
+                    approx_val_imp_approx_val_sup 
+                    approx_loc_imp_approx_loc_sup
              simp add: defs1 map_eq_Cons)
 done
 
@@ -539,7 +565,9 @@
   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
 ==> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1 map_eq_Cons)
-apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
+apply (force intro: approx_stk_imp_approx_stk_sup 
+                    approx_val_imp_approx_val_sup 
+                    approx_loc_imp_approx_loc_sup
              simp add: defs1 map_eq_Cons)
 done
 
@@ -552,7 +580,9 @@
   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
 ==> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1 map_eq_Cons approx_val_def conf_def)
-apply (blast intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup)
+apply (blast intro: approx_stk_imp_approx_stk_sup 
+                    approx_val_imp_approx_val_sup 
+                    approx_loc_imp_approx_loc_sup)
 done
 
 
@@ -572,10 +602,11 @@
 prefer 9
 apply (blast intro: Return_correct)
 apply (unfold wt_jvm_prog_def)
-apply (fast intro: Load_correct Store_correct Bipush_correct Aconst_null_correct 
-       Checkcast_correct Getfield_correct Putfield_correct New_correct 
-       Goto_correct Ifcmpeq_correct Pop_correct Dup_correct 
-       Dup_x1_correct Dup_x2_correct Swap_correct IAdd_correct)+
+apply (fast intro: 
+  Load_correct Store_correct Bipush_correct Aconst_null_correct 
+  Checkcast_correct Getfield_correct Putfield_correct New_correct 
+  Goto_correct Ifcmpeq_correct Pop_correct Dup_correct 
+  Dup_x1_correct Dup_x2_correct Swap_correct IAdd_correct)+
 done
 
 
@@ -627,11 +658,14 @@
 
 
 theorem BV_correct_initial:
-"[| wt_jvm_prog G phi; G \<turnstile> s0 -jvm-> (None,hp,(stk,loc,C,sig,pc)#frs); G,phi \<turnstile>JVM s0 \<surd>|] 
- ==>  approx_stk G hp stk (fst (the (((phi  C)  sig) ! pc))) \<and> approx_loc G hp loc (snd (the (((phi  C)  sig) ! pc)))"
+"[| wt_jvm_prog G phi; 
+    G \<turnstile> s0 -jvm-> (None,hp,(stk,loc,C,sig,pc)#frs); G,phi \<turnstile>JVM s0 \<surd>|] 
+==> approx_stk G hp stk (fst (the (((phi  C)  sig) ! pc))) \<and> 
+    approx_loc G hp loc (snd (the (((phi  C)  sig) ! pc)))"
 apply (drule BV_correct)
 apply assumption+
-apply (simp add: correct_state_def correct_frame_def split_def split: option.splits)
+apply (simp add: correct_state_def correct_frame_def split_def 
+            split: option.splits)
 done
 
 end
diff -r 2264bdd8becc -r 9f84ffa4a8d0 src/HOL/MicroJava/BV/Convert.thy
--- a/src/HOL/MicroJava/BV/Convert.thy	Thu Sep 21 18:58:25 2000 +0200
+++ b/src/HOL/MicroJava/BV/Convert.thy	Thu Sep 21 19:25:57 2000 +0200
@@ -40,11 +40,13 @@
 
   (* lifts a relation to option with None as bottom element *)
   lift_bottom :: "('a => 'b => bool) => ('a option => 'b option => bool)"
-  "lift_bottom P a' a == case a' of 
-                          None    => True 
-                        | Some t' => (case a of None => False | Some t => P t' t)"
+  "lift_bottom P a' a == 
+   case a' of 
+     None    => True 
+   | Some t' => (case a of None => False | Some t => P t' t)"
 
-  sup_ty_opt :: "['code prog,ty err,ty err] => bool" ("_ \<turnstile> _ <=o _" [71,71] 70)
+  sup_ty_opt :: "['code prog,ty err,ty err] => bool" 
+                 ("_ \<turnstile> _ <=o _" [71,71] 70)
   "sup_ty_opt G == lift_top (\<lambda>t t'. G \<turnstile> t \<preceq> t')"
 
   sup_loc :: "['code prog,locvars_type,locvars_type] => bool" 
@@ -53,17 +55,22 @@
 
   sup_state :: "['code prog,state_type,state_type] => bool"	  
                ("_ \<turnstile> _ <=s _"  [71,71] 70)
-  "G \<turnstile> s <=s s' == (G \<turnstile> map Ok (fst s) <=l map Ok (fst s')) \<and> G \<turnstile> snd s <=l snd s'"
+  "G \<turnstile> s <=s s' == 
+   (G \<turnstile> map Ok (fst s) <=l map Ok (fst s')) \<and> G \<turnstile> snd s <=l snd s'"
 
   sup_state_opt :: "['code prog,state_type option,state_type option] => bool" 
                    ("_ \<turnstile> _ <=' _"  [71,71] 70)
   "sup_state_opt G == lift_bottom (\<lambda>t t'. G \<turnstile> t <=s t')"
 
 syntax (HTML output) 
-  sup_ty_opt :: "['code prog,ty err,ty err] => bool" ("_ |- _ <=o _")
-  sup_loc :: "['code prog,locvars_type,locvars_type] => bool" ("_ |- _ <=l _"  [71,71] 70)
-  sup_state :: "['code prog,state_type,state_type] => bool"	("_ |- _ <=s _"  [71,71] 70)
-  sup_state_opt :: "['code prog,state_type option,state_type option] => bool" ("_ |- _ <=' _"  [71,71] 70)
+  sup_ty_opt    :: "['code prog,ty err,ty err] => bool" 
+                   ("_ |- _ <=o _")
+  sup_loc       :: "['code prog,locvars_type,locvars_type] => bool" 
+                   ("_ |- _ <=l _"  [71,71] 70)
+  sup_state     :: "['code prog,state_type,state_type] => bool"	
+                   ("_ |- _ <=s _"  [71,71] 70)
+  sup_state_opt :: "['code prog,state_type option,state_type option] => bool"
+                   ("_ |- _ <=' _"  [71,71] 70)
                    
 
 lemma not_Err_eq [iff]:
@@ -80,7 +87,7 @@
   by (simp add: lift_top_def split: err.splits)
 
 lemma lift_top_trans [trans]:
-  "[| !!x y z. [| P x y; P y z |] ==> P x z; lift_top P x y; lift_top P y z |] 
+  "[| !!x y z. [| P x y; P y z |] ==> P x z; lift_top P x y; lift_top P y z |]
   ==> lift_top P x z"
 proof -
   assume [trans]: "!!x y z. [| P x y; P y z |] ==> P x z"
@@ -141,7 +148,8 @@
   by (simp add: lift_bottom_def split: option.splits)
 
 lemma lift_bottom_trans [trans]:
-  "[| !!x y z. [| P x y; P y z |] ==> P x z; lift_bottom P x y; lift_bottom P y z |]
+  "[| !!x y z. [| P x y; P y z |] ==> P x z; 
+      lift_bottom P x y; lift_bottom P y z |]
   ==> lift_bottom P x z"
 proof -
   assume [trans]: "!!x y z. [| P x y; P y z |] ==> P x z"
@@ -286,8 +294,8 @@
 
 
 theorem all_nth_sup_loc:
-  "\<forall>b. length a = length b --> (\<forall> n. n < length a --> (G \<turnstile> (a!n) <=o (b!n))) --> 
-       (G \<turnstile> a <=l b)" (is "?P a")
+  "\<forall>b. length a = length b --> (\<forall> n. n < length a --> (G \<turnstile> (a!n) <=o (b!n))) 
+  --> (G \<turnstile> a <=l b)" (is "?P a")
 proof (induct a)
   show "?P []" by simp
 
diff -r 2264bdd8becc -r 9f84ffa4a8d0 src/HOL/MicroJava/BV/Correct.thy
--- a/src/HOL/MicroJava/BV/Correct.thy	Thu Sep 21 18:58:25 2000 +0200
+++ b/src/HOL/MicroJava/BV/Correct.thy	Thu Sep 21 19:25:57 2000 +0200
@@ -6,27 +6,29 @@
 The invariant for the type safety proof.
 *)
 
-header "Type Safety Invariant"
+header "BV Type Safety Invariant"
 
 theory Correct = BVSpec:
 
 constdefs
- approx_val :: "[jvm_prog,aheap,val,ty err] => bool"
-"approx_val G h v any == case any of Err => True | Ok T => G,h\<turnstile>v::\<preceq>T"
+  approx_val :: "[jvm_prog,aheap,val,ty err] => bool"
+  "approx_val G h v any == case any of Err => True | Ok T => G,h\<turnstile>v::\<preceq>T"
 
- approx_loc :: "[jvm_prog,aheap,val list,locvars_type] => bool"
-"approx_loc G hp loc LT == list_all2 (approx_val G hp) loc LT"
+  approx_loc :: "[jvm_prog,aheap,val list,locvars_type] => bool"
+  "approx_loc G hp loc LT == list_all2 (approx_val G hp) loc LT"
+
+  approx_stk :: "[jvm_prog,aheap,opstack,opstack_type] => bool"
+  "approx_stk G hp stk ST == approx_loc G hp stk (map Ok ST)"
 
- approx_stk :: "[jvm_prog,aheap,opstack,opstack_type] => bool"
-"approx_stk G hp stk ST == approx_loc G hp stk (map Ok ST)"
+  correct_frame  :: "[jvm_prog,aheap,state_type,nat,bytecode] => frame => bool"
+  "correct_frame G hp == \<lambda>(ST,LT) maxl ins (stk,loc,C,sig,pc).
+                         approx_stk G hp stk ST  \<and> approx_loc G hp loc LT \<and> 
+                         pc < length ins \<and> length loc=length(snd sig)+maxl+1"
 
- correct_frame  :: "[jvm_prog,aheap,state_type,nat,bytecode] => frame => bool"
-"correct_frame G hp == \<lambda>(ST,LT) maxl ins (stk,loc,C,sig,pc).
-   approx_stk G hp stk ST  \<and> approx_loc G hp loc LT \<and> 
-   pc < length ins \<and> length loc=length(snd sig)+maxl+1"
-
- correct_frame_opt :: "[jvm_prog,aheap,state_type option,nat,bytecode] => frame => bool"
-"correct_frame_opt G hp s == case s of None => \<lambda>maxl ins f. False | Some t => correct_frame G hp t"
+  correct_frame_opt :: "[jvm_prog,aheap,state_type option,nat,bytecode] 
+                        => frame => bool"
+  "correct_frame_opt G hp s == 
+    case s of None => \<lambda>maxl ins f. False | Some t => correct_frame G hp t"
 
 
 consts
@@ -75,7 +77,7 @@
 apply clarsimp
 apply (drule newref_None 1) back
 apply simp
-.
+done
 
 lemma sup_heap_update_value:
   "hp a = Some (C,od') ==> hp \<le>| hp (a \<mapsto> (C,od))"
@@ -93,14 +95,15 @@
 by (auto intro: null simp add: approx_val_def)
 
 lemma approx_val_imp_approx_val_assConvertible [rule_format]: 
-  "wf_prog wt G ==> approx_val G hp v (Ok T) --> G\<turnstile> T\<preceq>T' --> approx_val G hp v (Ok T')"
+  "wf_prog wt G ==> approx_val G hp v (Ok T) --> G\<turnstile> T\<preceq>T' 
+  --> approx_val G hp v (Ok T')"
 by (cases T) (auto intro: conf_widen simp add: approx_val_def)
 
 lemma approx_val_imp_approx_val_sup_heap [rule_format]:
   "approx_val G hp v at --> hp \<le>| hp' --> approx_val G hp' v at"
 apply (simp add: approx_val_def split: err.split)
 apply (blast intro: conf_hext)
-.
+done
 
 lemma approx_val_imp_approx_val_heap_update:
   "[|hp a = Some obj'; G,hp\<turnstile> v::\<preceq>T; obj_ty obj = obj_ty obj'|] 
@@ -108,24 +111,28 @@
 by (cases v, auto simp add: obj_ty_def conf_def)
 
 lemma approx_val_imp_approx_val_sup [rule_format]:
-  "wf_prog wt G ==> (approx_val G h v us) --> (G \<turnstile> us <=o us') --> (approx_val G h v us')"
+  "wf_prog wt G ==> (approx_val G h v us) --> (G \<turnstile> us <=o us') 
+  --> (approx_val G h v us')"
 apply (simp add: sup_PTS_eq approx_val_def split: err.split)
 apply (blast intro: conf_widen)
-.
+done
 
 lemma approx_loc_imp_approx_val_sup:
-  "[|wf_prog wt G; approx_loc G hp loc LT; idx < length LT; v = loc!idx; G \<turnstile> LT!idx <=o at|]
+  "[| wf_prog wt G; approx_loc G hp loc LT; idx < length LT; 
+      v = loc!idx; G \<turnstile> LT!idx <=o at |]
   ==> approx_val G hp v at"
 apply (unfold approx_loc_def)
 apply (unfold list_all2_def)
-apply (auto intro: approx_val_imp_approx_val_sup simp add: split_def all_set_conv_all_nth)
-.
+apply (auto intro: approx_val_imp_approx_val_sup 
+            simp add: split_def all_set_conv_all_nth)
+done
 
 
 (** approx_loc **)
 
 lemma approx_loc_Cons [iff]:
-  "approx_loc G hp (s#xs) (l#ls) = (approx_val G hp s l \<and> approx_loc G hp xs ls)"
+  "approx_loc G hp (s#xs) (l#ls) = 
+  (approx_val G hp s l \<and> approx_loc G hp xs ls)"
 by (simp add: approx_loc_def)
 
 lemma assConv_approx_stk_imp_approx_loc [rule_format]:
@@ -136,25 +143,27 @@
 apply (clarsimp simp add: all_set_conv_all_nth)
 apply (rule approx_val_imp_approx_val_assConvertible)
 apply auto
-.
+done
 
 
 lemma approx_loc_imp_approx_loc_sup_heap [rule_format]:
-  "\<forall>lvars. approx_loc G hp lvars lt --> hp \<le>| hp' --> approx_loc G hp' lvars lt"
+  "\<forall>lvars. approx_loc G hp lvars lt --> hp \<le>| hp' 
+  --> approx_loc G hp' lvars lt"
 apply (unfold approx_loc_def list_all2_def)
 apply (cases lt)
  apply simp
 apply clarsimp
 apply (rule approx_val_imp_approx_val_sup_heap)
 apply auto
-.
+done
 
 lemma approx_loc_imp_approx_loc_sup [rule_format]:
-  "wf_prog wt G ==> approx_loc G hp lvars lt --> G \<turnstile> lt <=l lt' --> approx_loc G hp lvars lt'"
+  "wf_prog wt G ==> approx_loc G hp lvars lt --> G \<turnstile> lt <=l lt' 
+  --> approx_loc G hp lvars lt'"
 apply (unfold sup_loc_def approx_loc_def list_all2_def)
 apply (auto simp add: all_set_conv_all_nth)
 apply (auto elim: approx_val_imp_approx_val_sup)
-.
+done
 
 
 lemma approx_loc_imp_approx_loc_subst [rule_format]:
@@ -162,18 +171,19 @@
   --> (approx_loc G hp (loc[idx:=x]) (LT[idx:=X]))"
 apply (unfold approx_loc_def list_all2_def)
 apply (auto dest: subsetD [OF set_update_subset_insert] simp add: zip_update)
-.
+done
 
 
 lemmas [cong] = conj_cong 
 
 lemma approx_loc_append [rule_format]:
   "\<forall>L1 l2 L2. length l1=length L1 --> 
-  approx_loc G hp (l1@l2) (L1@L2) = (approx_loc G hp l1 L1 \<and> approx_loc G hp l2 L2)"
+  approx_loc G hp (l1@l2) (L1@L2) = 
+  (approx_loc G hp l1 L1 \<and> approx_loc G hp l2 L2)"
 apply (unfold approx_loc_def list_all2_def)
 apply simp
 apply blast
-.
+done
 
 lemmas [cong del] = conj_cong
 
@@ -184,7 +194,7 @@
   "approx_stk G hp (rev s) (rev t) = approx_stk G hp s t"
 apply (unfold approx_stk_def approx_loc_def list_all2_def)
 apply (auto simp add: zip_rev sym [OF rev_map])
-.
+done
 
 lemma approx_stk_rev:
   "approx_stk G hp (rev s) t = approx_stk G hp s (rev t)"
@@ -192,7 +202,8 @@
 
 
 lemma approx_stk_imp_approx_stk_sup_heap [rule_format]:
-  "\<forall>lvars. approx_stk G hp lvars lt --> hp \<le>| hp' --> approx_stk G hp' lvars lt"
+  "\<forall>lvars. approx_stk G hp lvars lt --> hp \<le>| hp' 
+  --> approx_stk G hp' lvars lt"
 by (auto intro: approx_loc_imp_approx_loc_sup_heap simp add: approx_stk_def)
 
 lemma approx_stk_imp_approx_stk_sup [rule_format]:
@@ -229,7 +240,7 @@
 apply (unfold oconf_def lconf_def)
 apply (simp add: map_of_map)
 apply (force intro: defval_conf dest: map_of_SomeD is_type_fields)
-.
+done
 
 
 lemma oconf_imp_oconf_field_update [rule_format]:
@@ -243,7 +254,7 @@
 apply (unfold oconf_def lconf_def)
 apply simp
 apply (fast intro: conf_hext sup_heap_newref)
-.
+done
 
 
 lemma oconf_imp_oconf_heap_update [rule_format]:
@@ -252,7 +263,7 @@
 apply (unfold oconf_def lconf_def)
 apply simp
 apply (force intro: approx_val_imp_approx_val_heap_update)
-.
+done
 
 
 (** hconf **)
@@ -262,7 +273,7 @@
   "hp x = None --> G\<turnstile>h hp\<surd> --> G,hp\<turnstile>obj\<surd> --> G\<turnstile>h hp(newref hp\<mapsto>obj)\<surd>"
 apply (simp add: hconf_def)
 apply (fast intro: oconf_imp_oconf_heap_newref)
-.
+done
 
 lemma hconf_imp_hconf_field_update [rule_format]:
   "map_of (fields (G, oT)) (F, D) = Some T \<and> hp oloc = Some(oT,fs) \<and> 
@@ -270,7 +281,7 @@
 apply (simp add: hconf_def)
 apply (force intro: oconf_imp_oconf_heap_update oconf_imp_oconf_field_update 
              simp add: obj_ty_def)
-.
+done
 
 (** correct_frames **)
 
@@ -297,7 +308,7 @@
  apply simp
 apply (rule sup_heap_update_value)
 apply simp
-.
+done
 
 lemma correct_frames_imp_correct_frames_newref [rule_format]:
   "\<forall>rT C sig. hp x = None --> correct_frames G hp phi rT sig frs \<and> oconf G hp obj 
@@ -318,7 +329,7 @@
  apply simp
 apply (rule sup_heap_newref)
 apply simp
-.
+done
 
 end
 
diff -r 2264bdd8becc -r 9f84ffa4a8d0 src/HOL/MicroJava/J/Eval.thy
--- a/src/HOL/MicroJava/J/Eval.thy	Thu Sep 21 18:58:25 2000 +0200
+++ b/src/HOL/MicroJava/J/Eval.thy	Thu Sep 21 19:25:57 2000 +0200
@@ -15,113 +15,115 @@
   exec  :: "java_mb prog => (xstate \\<times> stmt                 \\<times> xstate) set"
 
 syntax
-  eval :: "[java_mb prog,xstate,expr,val,xstate] => bool "("_\\<turnstile>_ -_\\<succ>_-> _"[51,82,82,82,82]81)
+  eval :: "[java_mb prog,xstate,expr,val,xstate] => bool "
+          ("_\\<turnstile>_ -_\\<succ>_-> _"[51,82,82,82,82]81)
   evals:: "[java_mb prog,xstate,expr list,
-	                      val list,xstate] => bool "("_\\<turnstile>_ -_[\\<succ>]_-> _"[51,82,51,51,82]81)
-  exec :: "[java_mb prog,xstate,stmt,    xstate] => bool "("_\\<turnstile>_ -_-> _"  [51,82,82,   82]81)
+                        val list,xstate] => bool "
+          ("_\\<turnstile>_ -_[\\<succ>]_-> _"[51,82,51,51,82]81)
+  exec :: "[java_mb prog,xstate,stmt,    xstate] => bool "
+          ("_\\<turnstile>_ -_-> _"  [51,82,82,   82]81)
 
 translations
   "G\\<turnstile>s -e \\<succ> v-> (x,s')" <= "(s, e, v, x, s') \\<in> eval  G"
-  "G\\<turnstile>s -e \\<succ> v->    s' " == "(s, e, v,    s' ) \\<in> eval  G"
+  "G\\<turnstile>s -e \\<succ> v->    s' " == "(s, e, v,    s') \\<in> eval  G"
   "G\\<turnstile>s -e[\\<succ>]v-> (x,s')" <= "(s, e, v, x, s') \\<in> evals G"
-  "G\\<turnstile>s -e[\\<succ>]v->    s' " == "(s, e, v,    s' ) \\<in> evals G"
-  "G\\<turnstile>s -c    -> (x,s')" <= "(s, c, x, s') \\<in> exec  G"
-  "G\\<turnstile>s -c    ->    s' " == "(s, c,    s') \\<in> exec  G"
+  "G\\<turnstile>s -e[\\<succ>]v->    s' " == "(s, e, v,    s') \\<in> evals G"
+  "G\\<turnstile>s -c    -> (x,s')" <= "(s, c, x, s') \\<in> exec G"
+  "G\\<turnstile>s -c    ->    s' " == "(s, c,    s') \\<in> exec G"
 
 inductive "eval G" "evals G" "exec G" intrs
 
 (* evaluation of expressions *)
 
   (* cf. 15.5 *)
-  XcptE				  "G\\<turnstile>(Some xc,s) -e\\<succ>arbitrary-> (Some xc,s)"
+  XcptE "G\\<turnstile>(Some xc,s) -e\\<succ>arbitrary-> (Some xc,s)"
 
   (* cf. 15.8.1 *)
-  NewC	"[|h = heap s; (a,x) = new_Addr h;
-	  h'= h(a\\<mapsto>(C,init_vars (fields (G,C))))|] ==>
-				   G\\<turnstile>Norm s -NewC C\\<succ>Addr a-> c_hupd h' (x,s)"
+  NewC  "[| h = heap s; (a,x) = new_Addr h;
+            h'= h(a\\<mapsto>(C,init_vars (fields (G,C)))) |] ==>
+         G\\<turnstile>Norm s -NewC C\\<succ>Addr a-> c_hupd h' (x,s)"
 
   (* cf. 15.15 *)
-  Cast	"[|G\\<turnstile>Norm s0 -e\\<succ>v-> (x1,s1);
-	  x2=raise_if (\\<not> cast_ok G C (heap s1) v) ClassCast x1|] ==>
-			        G\\<turnstile>Norm s0 -Cast C e\\<succ>v-> (x2,s1)"
+  Cast  "[| G\\<turnstile>Norm s0 -e\\<succ>v-> (x1,s1);
+            x2 = raise_if (\\<not> cast_ok G C (heap s1) v) ClassCast x1 |] ==>
+         G\\<turnstile>Norm s0 -Cast C e\\<succ>v-> (x2,s1)"
 
   (* cf. 15.7.1 *)
-  Lit				   "G\\<turnstile>Norm s -Lit v\\<succ>v-> Norm s"
+  Lit   "G\\<turnstile>Norm s -Lit v\\<succ>v-> Norm s"
 
-  BinOp "[|G\\<turnstile>Norm s -e1\\<succ>v1-> s1;
-	  G\\<turnstile>s1     -e2\\<succ>v2-> s2;
-	  v = (case bop of Eq  => Bool (v1 = v2)
-	                 | Add => Intg (the_Intg v1 + the_Intg v2))|] ==>
-				   G\\<turnstile>Norm s -BinOp bop e1 e2\\<succ>v-> s2"
+  BinOp "[| G\\<turnstile>Norm s -e1\\<succ>v1-> s1;
+            G\\<turnstile>s1     -e2\\<succ>v2-> s2;
+            v = (case bop of Eq  => Bool (v1 = v2)
+                           | Add => Intg (the_Intg v1 + the_Intg v2)) |] ==>
+         G\\<turnstile>Norm s -BinOp bop e1 e2\\<succ>v-> s2"
 
   (* cf. 15.13.1, 15.2 *)
-  LAcc				  "G\\<turnstile>Norm s -LAcc v\\<succ>the (locals s v)-> Norm s"
+  LAcc  "G\\<turnstile>Norm s -LAcc v\\<succ>the (locals s v)-> Norm s"
 
   (* cf. 15.25.1 *)
-  LAss  "[|G\\<turnstile>Norm s -e\\<succ>v->  (x,(h,l));
-	  l' = (if x = None then l(va\\<mapsto>v) else l)|] ==>
-				   G\\<turnstile>Norm s -va::=e\\<succ>v-> (x,(h,l'))"
+  LAss  "[| G\\<turnstile>Norm s -e\\<succ>v-> (x,(h,l));
+            l' = (if x = None then l(va\\<mapsto>v) else l) |] ==>
+         G\\<turnstile>Norm s -va::=e\\<succ>v-> (x,(h,l'))"
 
 
   (* cf. 15.10.1, 15.2 *)
-  FAcc	"[|G\\<turnstile>Norm s0 -e\\<succ>a'-> (x1,s1); 
-	  v = the (snd (the (heap s1 (the_Addr a'))) (fn,T))|] ==>
-				 G\\<turnstile>Norm s0 -{T}e..fn\\<succ>v-> (np a' x1,s1)"
+  FAcc  "[| G\\<turnstile>Norm s0 -e\\<succ>a'-> (x1,s1); 
+            v = the (snd (the (heap s1 (the_Addr a'))) (fn,T)) |] ==>
+         G\\<turnstile>Norm s0 -{T}e..fn\\<succ>v-> (np a' x1,s1)"
 
   (* cf. 15.25.1 *)
-  FAss  "[|G\\<turnstile>     Norm s0  -e1\\<succ>a'-> (x1,s1); a = the_Addr a';
-	  G\\<turnstile>(np a' x1,s1) -e2\\<succ>v -> (x2,s2);
-	  h = heap s2; (c,fs) = the (h a);
-	  h' = h(a\\<mapsto>(c,(fs((fn,T)\\<mapsto>v))))|] ==>
-			  G\\<turnstile>Norm s0 -{T}e1..fn:=e2\\<succ>v-> c_hupd h' (x2,s2)"
+  FAss  "[| G\\<turnstile>     Norm s0  -e1\\<succ>a'-> (x1,s1); a = the_Addr a';
+            G\\<turnstile>(np a' x1,s1) -e2\\<succ>v -> (x2,s2);
+            h  = heap s2; (c,fs) = the (h a);
+            h' = h(a\\<mapsto>(c,(fs((fn,T)\\<mapsto>v)))) |] ==>
+         G\\<turnstile>Norm s0 -{T}e1..fn:=e2\\<succ>v-> c_hupd h' (x2,s2)"
 
   (* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5, 14.15 *)
-  Call	"[|G\\<turnstile>Norm s0 -e\\<succ>a'-> s1; a = the_Addr a';
-	   G\\<turnstile>s1 -ps[\\<succ>]pvs-> (x,(h,l)); dynT = fst (the (h a));
-	   (md,rT,pns,lvars,blk,res) = the (method (G,dynT) (mn,pTs));
-	   G\\<turnstile>(np a' x,(h,(init_vars lvars)(pns[\\<mapsto>]pvs)(This\\<mapsto>a'))) -blk-> s3;
-	   G\\<turnstile>     s3 -res\\<succ>v -> (x4,s4)|] ==>
-			    G\\<turnstile>Norm s0 -e..mn({pTs}ps)\\<succ>v-> (x4,(heap s4,l))"
+  Call  "[| G\\<turnstile>Norm s0 -e\\<succ>a'-> s1; a = the_Addr a';
+            G\\<turnstile>s1 -ps[\\<succ>]pvs-> (x,(h,l)); dynT = fst (the (h a));
+            (md,rT,pns,lvars,blk,res) = the (method (G,dynT) (mn,pTs));
+            G\\<turnstile>(np a' x,(h,(init_vars lvars)(pns[\\<mapsto>]pvs)(This\\<mapsto>a'))) -blk-> s3;
+            G\\<turnstile> s3 -res\\<succ>v -> (x4,s4) |] ==>
+         G\\<turnstile>Norm s0 -e..mn({pTs}ps)\\<succ>v-> (x4,(heap s4,l))"
 
 
 (* evaluation of expression lists *)
 
   (* cf. 15.5 *)
-  XcptEs			  "G\\<turnstile>(Some xc,s) -e[\\<succ>]arbitrary-> (Some xc,s)"
+  XcptEs "G\\<turnstile>(Some xc,s) -e[\\<succ>]arbitrary-> (Some xc,s)"
 
   (* cf. 15.11.??? *)
-  Nil
-				    "G\\<turnstile>Norm s0 -[][\\<succ>][]-> Norm s0"
+  Nil   "G\\<turnstile>Norm s0 -[][\\<succ>][]-> Norm s0"
 
   (* cf. 15.6.4 *)
-  Cons	"[|G\\<turnstile>Norm s0 -e  \\<succ> v -> s1;
-           G\\<turnstile>     s1 -es[\\<succ>]vs-> s2|] ==>
-				   G\\<turnstile>Norm s0 -e#es[\\<succ>]v#vs-> s2"
+  Cons  "[| G\\<turnstile>Norm s0 -e  \\<succ> v -> s1;
+            G\\<turnstile>     s1 -es[\\<succ>]vs-> s2 |] ==>
+         G\\<turnstile>Norm s0 -e#es[\\<succ>]v#vs-> s2"
 
 (* execution of statements *)
 
   (* cf. 14.1 *)
-  XcptS				 "G\\<turnstile>(Some xc,s) -s0-> (Some xc,s)"
+  XcptS "G\\<turnstile>(Some xc,s) -s0-> (Some xc,s)"
 
   (* cf. 14.5 *)
-  Skip	 			    "G\\<turnstile>Norm s -Skip-> Norm s"
+  Skip  "G\\<turnstile>Norm s -Skip-> Norm s"
 
   (* cf. 14.7 *)
-  Expr	"[|G\\<turnstile>Norm s0 -e\\<succ>v-> s1|] ==>
-				  G\\<turnstile>Norm s0 -Expr e-> s1"
+  Expr  "[| G\\<turnstile>Norm s0 -e\\<succ>v-> s1 |] ==>
+         G\\<turnstile>Norm s0 -Expr e-> s1"
 
   (* cf. 14.2 *)
-  Comp	"[|G\\<turnstile>Norm s0 -s -> s1;
-	  G\\<turnstile>     s1 -t -> s2|] ==>
-				 G\\<turnstile>Norm s0 -(s;; t)-> s2"
+  Comp  "[| G\\<turnstile>Norm s0 -s -> s1;
+            G\\<turnstile> s1 -t -> s2|] ==>
+         G\\<turnstile>Norm s0 -(s;; t)-> s2"
 
   (* cf. 14.8.2 *)
-  Cond	"[|G\\<turnstile>Norm s0  -e \\<succ>v-> s1;
-	  G\\<turnstile>     s1 -(if  the_Bool v then s else t)-> s2|] ==>
-		        G\\<turnstile>Norm s0 -(If(e) s Else t)-> s2"
+  Cond  "[| G\\<turnstile>Norm s0  -e \\<succ>v-> s1;
+            G\\<turnstile> s1 -(if  the_Bool v then s else t)-> s2|] ==>
+         G\\<turnstile>Norm s0 -(If(e) s Else t)-> s2"
 
   (* cf. 14.10, 14.10.1 *)
-  Loop	"[|G\\<turnstile>Norm s0 -(If(e) (s;; While(e) s) Else Skip)-> s1|] ==>
-			    G\\<turnstile>Norm s0 -(While(e) s)-> s1"
+  Loop  "[| G\\<turnstile>Norm s0 -(If(e) (s;; While(e) s) Else Skip)-> s1 |] ==>
+         G\\<turnstile>Norm s0 -(While(e) s)-> s1"
 
 end
diff -r 2264bdd8becc -r 9f84ffa4a8d0 src/HOL/MicroJava/JVM/JVMExecInstr.thy
--- a/src/HOL/MicroJava/JVM/JVMExecInstr.thy	Thu Sep 21 18:58:25 2000 +0200
+++ b/src/HOL/MicroJava/JVM/JVMExecInstr.thy	Thu Sep 21 19:25:57 2000 +0200
@@ -9,7 +9,8 @@
 JVMExecInstr = JVMInstructions + JVMState +
 
 consts
-exec_instr :: "[instr, jvm_prog, aheap, opstack, locvars, cname, sig, p_count, frame list] => jvm_state"
+  exec_instr :: "[instr, jvm_prog, aheap, opstack, locvars, 
+                  cname, sig, p_count, frame list] => jvm_state"
 primrec
  "exec_instr (Load idx) G hp stk vars Cl sig pc frs = 
       (None, hp, ((vars ! idx) # stk, vars, Cl, sig, pc+1)#frs)"
@@ -63,9 +64,9 @@
 	     xp'	= raise_xcpt (oref=Null) NullPointer;
 	     dynT	= fst(the(hp(the_Addr oref)));
 	     (dc,mh,mxl,c)= the (method (G,dynT) (mn,ps));
-	     frs'	= if xp'=None
-	                  then [([],rev argsoref@replicate mxl arbitrary,dc,(mn,ps),0)]
-	                  else []
+	     frs'	= if xp'=None then 
+                [([],rev argsoref@replicate mxl arbitrary,dc,(mn,ps),0)]
+	            else []
 	 in
       (xp', hp, frs'@(drop (n+1) stk, vars, Cl, sig, pc+1)#frs))"
 
@@ -84,11 +85,13 @@
       (None, hp, (hd stk # stk, vars, Cl, sig, pc+1)#frs)"
 
  "exec_instr Dup_x1 G hp stk vars Cl sig pc frs = 
-      (None, hp, (hd stk # hd (tl stk) # hd stk # (tl (tl stk)), vars, Cl, sig, pc+1)#frs)"
+      (None, hp, (hd stk # hd (tl stk) # hd stk # (tl (tl stk)), 
+                  vars, Cl, sig, pc+1)#frs)"
 
  "exec_instr Dup_x2 G hp stk vars Cl sig pc frs = 
-      (None, hp, (hd stk # hd (tl stk) # (hd (tl (tl stk))) # hd stk # (tl (tl (tl stk))),
-                  vars, Cl, sig, pc+1)#frs)"
+      (None, hp, 
+       (hd stk # hd (tl stk) # (hd (tl (tl stk))) # hd stk # (tl (tl (tl stk))),
+       vars, Cl, sig, pc+1)#frs)"
 
  "exec_instr Swap G hp stk vars Cl sig pc frs =
 	(let (val1,val2) = (hd stk,hd (tl stk))
@@ -98,7 +101,8 @@
  "exec_instr IAdd G hp stk vars Cl sig pc frs =
   (let (val1,val2) = (hd stk,hd (tl stk))
    in
-      (None, hp, (Intg ((the_Intg val1)+(the_Intg val2))#(tl (tl stk)), vars, Cl, sig, pc+1)#frs))"
+      (None, hp, (Intg ((the_Intg val1)+(the_Intg val2))#(tl (tl stk)), 
+       vars, Cl, sig, pc+1)#frs))"
 
  "exec_instr (Ifcmpeq i) G hp stk vars Cl sig pc frs =
 	(let (val1,val2) = (hd stk, hd (tl stk));