| changeset 9271 | c26964691975 |
| parent 9260 | 678e718a5a86 |
| child 9376 | c32c5696ec2a |
--- a/src/HOL/MicroJava/BV/BVSpec.thy Thu Jul 06 15:38:42 2000 +0200 +++ b/src/HOL/MicroJava/BV/BVSpec.thy Thu Jul 06 15:58:40 2000 +0200 @@ -129,7 +129,7 @@ (\\<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 = +"wt_OS IAdd G phi max_pc pc = (let (ST,LT) = phi ! pc in pc+1 < max_pc \\<and>