src/HOL/MicroJava/BV/Listn.thy
changeset 11225 01181fdbc9f0
parent 10918 9679326489cd
child 12516 d09d0f160888
     1.1 --- a/src/HOL/MicroJava/BV/Listn.thy	Mon Mar 26 16:31:38 2001 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/Listn.thy	Mon Mar 26 19:37:31 2001 +0200
     1.3 @@ -180,7 +180,6 @@
     1.4  lemma Cons_in_list_Suc [iff]:
     1.5    "(x#xs : list (Suc n) A) = (x:A & xs : list n A)";
     1.6  apply (simp add: in_list_Suc_iff)
     1.7 -apply blast
     1.8  done 
     1.9  
    1.10  lemma list_not_empty:
    1.11 @@ -332,7 +331,6 @@
    1.12  apply (simp add: in_list_Suc_iff)
    1.13  apply clarify
    1.14  apply simp
    1.15 -apply blast
    1.16  done 
    1.17  
    1.18  
    1.19 @@ -457,7 +455,6 @@
    1.20  apply (simp add: in_list_Suc_iff)
    1.21  apply clarify
    1.22  apply (simp add: plussub_def closed_err_lift2_conv)
    1.23 -apply blast
    1.24  done 
    1.25  
    1.26  lemma closed_lift2_sup: