1 -> 1'
authornipkow
Mon Aug 06 15:54:29 2001 +0200 (2001-08-06)
changeset 11466d64ccdeaf9ae
parent 11465 45d156ede468
child 11467 1064effe37f6
1 -> 1'
src/HOL/MicroJava/BV/Step.thy
     1.1 --- a/src/HOL/MicroJava/BV/Step.thy	Mon Aug 06 15:46:20 2001 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/Step.thy	Mon Aug 06 15:54:29 2001 +0200
     1.3 @@ -124,12 +124,12 @@
     1.4  proof -;
     1.5    assume "\<not>(2 < length a)"
     1.6    hence "length a < (Suc 2)" by simp
     1.7 -  hence * : "length a = 0 \<or> length a = 1 \<or> length a = 2" 
     1.8 +  hence * : "length a = 0 \<or> length a = 1' \<or> length a = 2" 
     1.9      by (auto simp add: less_Suc_eq)
    1.10  
    1.11    { 
    1.12      fix x 
    1.13 -    assume "length x = 1"
    1.14 +    assume "length x = 1'"
    1.15      hence "\<exists> l. x = [l]"  by - (cases x, auto)
    1.16    } note 0 = this
    1.17