--- a/src/HOL/MicroJava/BV/Err.thy Sat Jan 06 21:31:37 2001 +0100
+++ b/src/HOL/MicroJava/BV/Err.thy Sun Jan 07 18:43:13 2001 +0100
@@ -54,6 +54,13 @@
"err_semilat L" == "semilat(Err.sl L)"
+consts
+ strict :: "('a => 'b err) => ('a err => 'b err)"
+primrec
+ "strict f Err = Err"
+ "strict f (OK x) = f x"
+
+
lemma not_Err_eq:
"(x \<noteq> Err) = (\<exists>a. x = OK a)"
by (cases x) auto
@@ -63,6 +70,7 @@
by (cases x) auto
+
lemma unfold_lesub_err:
"e1 <=_(le r) e2 == le r e1 e2"
by (simp add: lesub_def)