# HG changeset patch
# User nipkow
# Date 985628251 -7200
# Node ID 01181fdbc9f01689a2b6a4a2bbce438cc50d5037
# Parent  5f10ca5e0b49784feab89db08375f9d3ea3fcdf1
simplified proofs

diff -r 5f10ca5e0b49 -r 01181fdbc9f0 src/HOL/MicroJava/BV/Err.thy
--- a/src/HOL/MicroJava/BV/Err.thy	Mon Mar 26 16:31:38 2001 +0200
+++ b/src/HOL/MicroJava/BV/Err.thy	Mon Mar 26 19:37:31 2001 +0200
@@ -139,7 +139,6 @@
   "semilat(A,r,f) ==> semilat(err A, Err.le r, lift2(%x y. OK(f x y)))"
 apply (unfold semilat_Def closed_def plussub_def lesub_def lift2_def Err.le_def err_def)
 apply (simp split: err.split)
-apply blast
 done
 
 lemma err_semilat_eslI: 
diff -r 5f10ca5e0b49 -r 01181fdbc9f0 src/HOL/MicroJava/BV/Listn.thy
--- a/src/HOL/MicroJava/BV/Listn.thy	Mon Mar 26 16:31:38 2001 +0200
+++ b/src/HOL/MicroJava/BV/Listn.thy	Mon Mar 26 19:37:31 2001 +0200
@@ -180,7 +180,6 @@
 lemma Cons_in_list_Suc [iff]:
   "(x#xs : list (Suc n) A) = (x:A & xs : list n A)";
 apply (simp add: in_list_Suc_iff)
-apply blast
 done 
 
 lemma list_not_empty:
@@ -332,7 +331,6 @@
 apply (simp add: in_list_Suc_iff)
 apply clarify
 apply simp
-apply blast
 done 
 
 
@@ -457,7 +455,6 @@
 apply (simp add: in_list_Suc_iff)
 apply clarify
 apply (simp add: plussub_def closed_err_lift2_conv)
-apply blast
 done 
 
 lemma closed_lift2_sup: