--- 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:
--- 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: