# HG changeset patch
# User nipkow
# Date 985617098 -7200
# Node ID 5f10ca5e0b49784feab89db08375f9d3ea3fcdf1
# Parent  fef9da0ee890caf2a40147927e61766ebe318e4d
simplified proofs

diff -r fef9da0ee890 -r 5f10ca5e0b49 src/HOL/BCV/Err.ML
--- a/src/HOL/BCV/Err.ML	Mon Mar 26 12:51:14 2001 +0200
+++ b/src/HOL/BCV/Err.ML	Mon Mar 26 16:31:38 2001 +0200
@@ -87,7 +87,6 @@
  [semilat_Def,closed_def,plussub_def,lesub_def,lift2_def,Err.le_def,err_def]
  "semilat(A,r,f) ==> semilat(err A, Err.le r, lift2(%x y. OK(f x y)))";
 by (asm_full_simp_tac (simpset() addsplits [err.split]) 1);
-by (Blast_tac 1);
 qed "semilat_errI";
 
 Goalw [sl_def,esl_def]
diff -r fef9da0ee890 -r 5f10ca5e0b49 src/HOL/BCV/Listn.ML
--- a/src/HOL/BCV/Listn.ML	Mon Mar 26 12:51:14 2001 +0200
+++ b/src/HOL/BCV/Listn.ML	Mon Mar 26 16:31:38 2001 +0200
@@ -115,7 +115,6 @@
 
 Goal "(x#xs : list (Suc n) A) = (x:A & xs : list n A)";
 by (simp_tac (simpset() addsimps [in_list_Suc_iff]) 1);
-by (Blast_tac 1);
 qed "Cons_in_list_Suc";
 AddIffs [Cons_in_list_Suc];