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