src/HOL/MicroJava/JVM/Opstack.thy

--- a/src/HOL/MicroJava/JVM/Opstack.thy	Thu Jul 06 11:24:09 2000 +0200
+++ b/src/HOL/MicroJava/JVM/Opstack.thy	Thu Jul 06 12:15:05 2000 +0200
@@ -17,6 +17,7 @@
  | Dup_x1
  | Dup_x2
  | Swap
+ | ADD
 	  
 consts
  exec_os :: "[op_stack,opstack,p_count] \\<Rightarrow> (opstack \\<times> p_count)" 
@@ -35,4 +36,9 @@
 	 in
 	 (val2#val1#(tl (tl stk)) , pc+1))"
 
+  "exec_os ADD stk pc =
+  (let (val1,val2) = (hd stk,hd (tl stk))
+   in
+   (Intg ((the_Intg val1)+(the_Intg val2))#(tl (tl stk)), pc+1))"
+
 end