| changeset 13187 | e5434b822a96 |
| parent 13148 | fe118a977a6d |
| child 13214 | 2aa33ed5f526 |
--- a/src/HOL/MicroJava/BV/BVExample.thy Thu May 30 10:12:11 2002 +0200 +++ b/src/HOL/MicroJava/BV/BVExample.thy Thu May 30 10:12:52 2002 +0200 @@ -174,8 +174,7 @@ lemma pc_next: "x \<in> [n0, n) \<Longrightarrow> P n0 \<Longrightarrow> (x \<in> [Suc n0, n) \<Longrightarrow> P x) \<Longrightarrow> P x" apply (cases "x=n0") - apply (auto simp add: intervall_def) - apply arith + apply (auto simp add: intervall_def) done lemma pc_end: "x \<in> [n,n) \<Longrightarrow> P x"