simplified proofs
authornipkow
Mon Mar 26 19:37:31 2001 +0200 (2001-03-26)
changeset 1122501181fdbc9f0
parent 11224 5f10ca5e0b49
child 11226 0adc5f9b4977
simplified proofs
src/HOL/MicroJava/BV/Err.thy
src/HOL/MicroJava/BV/Listn.thy
     1.1 --- a/src/HOL/MicroJava/BV/Err.thy	Mon Mar 26 16:31:38 2001 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/Err.thy	Mon Mar 26 19:37:31 2001 +0200
     1.3 @@ -139,7 +139,6 @@
     1.4    "semilat(A,r,f) ==> semilat(err A, Err.le r, lift2(%x y. OK(f x y)))"
     1.5  apply (unfold semilat_Def closed_def plussub_def lesub_def lift2_def Err.le_def err_def)
     1.6  apply (simp split: err.split)
     1.7 -apply blast
     1.8  done
     1.9  
    1.10  lemma err_semilat_eslI: 
     2.1 --- a/src/HOL/MicroJava/BV/Listn.thy	Mon Mar 26 16:31:38 2001 +0200
     2.2 +++ b/src/HOL/MicroJava/BV/Listn.thy	Mon Mar 26 19:37:31 2001 +0200
     2.3 @@ -180,7 +180,6 @@
     2.4  lemma Cons_in_list_Suc [iff]:
     2.5    "(x#xs : list (Suc n) A) = (x:A & xs : list n A)";
     2.6  apply (simp add: in_list_Suc_iff)
     2.7 -apply blast
     2.8  done 
     2.9  
    2.10  lemma list_not_empty:
    2.11 @@ -332,7 +331,6 @@
    2.12  apply (simp add: in_list_Suc_iff)
    2.13  apply clarify
    2.14  apply simp
    2.15 -apply blast
    2.16  done 
    2.17  
    2.18  
    2.19 @@ -457,7 +455,6 @@
    2.20  apply (simp add: in_list_Suc_iff)
    2.21  apply clarify
    2.22  apply (simp add: plussub_def closed_err_lift2_conv)
    2.23 -apply blast
    2.24  done 
    2.25  
    2.26  lemma closed_lift2_sup: