# HG changeset patch
# User kleing
# Date 962891920 -7200
# Node ID c26964691975173db5a54ba82436ce1350af7484
# Parent  7eff23d0b38066324c1378a3960c2e2fc7a80275
ADD -> IAdd

diff -r 7eff23d0b380 -r c26964691975 src/HOL/MicroJava/BV/BVSpec.thy
--- a/src/HOL/MicroJava/BV/BVSpec.thy	Thu Jul 06 15:38:42 2000 +0200
+++ b/src/HOL/MicroJava/BV/BVSpec.thy	Thu Jul 06 15:58:40 2000 +0200
@@ -129,7 +129,7 @@
 	 (\\<exists>ts ts' ST'. ST = ts' # ts # ST' \\<and> 	 
 		       G \\<turnstile> (ts # ts' # ST' , LT) <=s phi ! (pc+1)))"
 
-"wt_OS ADD G phi max_pc pc =
+"wt_OS IAdd G phi max_pc pc =
 	(let (ST,LT) = phi ! pc
 	 in
 	 pc+1 < max_pc \\<and>
diff -r 7eff23d0b380 -r c26964691975 src/HOL/MicroJava/BV/BVSpecTypeSafe.ML
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML	Thu Jul 06 15:38:42 2000 +0200
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML	Thu Jul 06 15:58:40 2000 +0200
@@ -514,14 +514,14 @@
 Goal 
 "\\<lbrakk> wf_prog wt G; \
 \  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins ! pc = OS ADD; \
+\  ins ! pc = OS IAdd; \
 \  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> \\<rbrakk> \
 \\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
 by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup]
   addss (simpset() addsimps [map_eq_Cons, approx_val_def]@defs1)) 1);
-qed "ADD_correct";
+qed "IAdd_correct";
 
 
 Goal
@@ -536,7 +536,7 @@
  ba 1;
 by(rewtac wt_jvm_prog_def);
 by (case_tac "os_com" 1);
-by (ALLGOALS (fast_tac (claset() addIs [Pop_correct,Dup_correct,Dup_x1_correct,Dup_x2_correct,Swap_correct,ADD_correct])));
+by (ALLGOALS (fast_tac (claset() addIs [Pop_correct,Dup_correct,Dup_x1_correct,Dup_x2_correct,Swap_correct,IAdd_correct])));
 qed "OS_correct";
 
 (** Main **)
diff -r 7eff23d0b380 -r c26964691975 src/HOL/MicroJava/BV/LBVSpec.thy
--- a/src/HOL/MicroJava/BV/LBVSpec.thy	Thu Jul 06 15:38:42 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy	Thu Jul 06 15:58:40 2000 +0200
@@ -130,7 +130,7 @@
 	 (\\<exists>ts ts' ST'. ST = ts' # ts # ST' \\<and> 	 
 		       (ts # ts' # ST' , LT) = s'))"
 
-"wtl_OS ADD s s' max_pc pc =
+"wtl_OS IAdd s s' max_pc pc =
 	(let (ST,LT) = s
 	 in
 	 pc+1 < max_pc \\<and>
diff -r 7eff23d0b380 -r c26964691975 src/HOL/MicroJava/JVM/Opstack.thy
--- a/src/HOL/MicroJava/JVM/Opstack.thy	Thu Jul 06 15:38:42 2000 +0200
+++ b/src/HOL/MicroJava/JVM/Opstack.thy	Thu Jul 06 15:58:40 2000 +0200
@@ -17,7 +17,7 @@
  | Dup_x1
  | Dup_x2
  | Swap
- | ADD
+ | IAdd
 	  
 consts
  exec_os :: "[op_stack,opstack,p_count] \\<Rightarrow> (opstack \\<times> p_count)" 
@@ -36,7 +36,7 @@
 	 in
 	 (val2#val1#(tl (tl stk)) , pc+1))"
 
-  "exec_os ADD stk pc =
+  "exec_os IAdd stk pc =
   (let (val1,val2) = (hd stk,hd (tl stk))
    in
    (Intg ((the_Intg val1)+(the_Intg val2))#(tl (tl stk)), pc+1))"