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