--- 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]
--- 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];