Pop elements in stack_1_2_op

pirapira · Oct 26, 2016 · 6caf6b7 · 6caf6b7
1 parent 8ebe453
commit 6caf6b7
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/ContractSem.thy b/ContractSem.thy
@@ -445,7 +445,7 @@ where
         (new0, new1) \<Rightarrow>
           InstructionContinue
             (venv_advance_pc c
-               v\<lparr>venv_stack := new0 # new1 # venv_stack v\<rparr>)))"
+               v\<lparr>venv_stack := new0 # new1 # t \<rparr>)))"
 
 text {* A general pattern of operations that take two words and produce one word: *}
 abbreviation stack_2_1_op ::