--- a/src/HOL/MicroJava/BV/BVSpec.thy Thu Jul 06 11:24:09 2000 +0200
+++ b/src/HOL/MicroJava/BV/BVSpec.thy Thu Jul 06 12:15:05 2000 +0200
@@ -129,6 +129,14 @@
(\\<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 =
+ (let (ST,LT) = phi ! pc
+ in
+ pc+1 < max_pc \\<and>
+ (\\<exists>ST'. ST = (PrimT Integer) # (PrimT Integer) # ST' \\<and>
+ G \\<turnstile> ((PrimT Integer) # ST' , LT) <=s phi ! (pc+1)))"
+
+
consts
wt_BR :: "[branch,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool"
primrec