src/HOL/MicroJava/BV/Err.thy
changeset 11225 01181fdbc9f0
parent 11085 b830bf10bf71
child 11549 e7265e70fd7c
--- 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: