# HG changeset patch
# User kleing
# Date 949768313 -3600
# Node ID 700067a98634c1f5fbdced67f848c0a139e0df55
# Parent  9e45cf2e6cf764b7c4fa0526dbe6935fdd6e6e87
Branch: top elements of stack only need to be convertible (not equal)

diff -r 9e45cf2e6cf7 -r 700067a98634 src/HOL/MicroJava/BV/BVSpec.thy
--- a/src/HOL/MicroJava/BV/BVSpec.thy	Sat Feb 05 17:06:27 2000 +0100
+++ b/src/HOL/MicroJava/BV/BVSpec.thy	Sat Feb 05 17:31:53 2000 +0100
@@ -136,9 +136,10 @@
 	(let (ST,LT) = phi ! pc
 	 in
 	 pc+1 < max_pc \\<and> (nat(int pc+branch)) < max_pc \\<and> 
-	 (\\<exists>ts ts' ST'. ST = ts # ts' # ST' \\<and>  ts = ts' \\<and>
+	 (\\<exists>ts ts' ST'. ST = ts # ts' # ST' \\<and>  (G \\<turnstile> ts \\<preceq> ts' \\<or> G \\<turnstile> ts' \\<preceq> ts) \\<and>
 		       G \\<turnstile> (ST' , LT) <=s phi ! (pc+1) \\<and>
 		       G \\<turnstile> (ST' , LT) <=s phi ! (nat(int pc+branch))))"
+
 "wt_BR (Goto branch) G phi max_pc pc =
 	(let (ST,LT) = phi ! pc
 	 in