| changeset 9271 | c26964691975 |
| parent 9260 | 678e718a5a86 |
| child 9376 | c32c5696ec2a |
--- a/src/HOL/MicroJava/BV/LBVSpec.thy Thu Jul 06 15:38:42 2000 +0200 +++ b/src/HOL/MicroJava/BV/LBVSpec.thy Thu Jul 06 15:58:40 2000 +0200 @@ -130,7 +130,7 @@ (\\<exists>ts ts' ST'. ST = ts' # ts # ST' \\<and> (ts # ts' # ST' , LT) = s'))" -"wtl_OS ADD s s' max_pc pc = +"wtl_OS IAdd s s' max_pc pc = (let (ST,LT) = s in pc+1 < max_pc \\<and>