diff -r 98f52cb93d93 -r ead84e90bfeb src/HOL/MicroJava/BV/Err.thy
--- 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)