Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/MicroJava/JVM/Opstack.thy
changeset 9271 c26964691975
parent 9260 678e718a5a86 
--- 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))"
isabelle