src/HOL/MicroJava/BV/LBVSpec.thy

 
 lemma err_semilatDorderI [simp, intro]:
   "err_semilat (A,r,f) \<Longrightarrow> order r"
   apply (simp add: Err.sl_def)
   apply (rule order_le_err [THEN iffD1])
-  apply (rule semilatDorderI)
+  apply (rule semilat.orderI)
   apply assumption
   done
 
 lemma err_opt_semilat [simp,elim]:
   "err_semilat (A,r,f) \<Longrightarrow> semilat (err (opt A), Err.le (Opt.le r), lift2 (Opt.sup f))"

     (is "?merge (l#ls) x = ?merge ls ?if'")
     by simp 
   also have "\<dots> = ?if ls ?if'" 
   proof -
     from l have "s' \<in> err (opt A)" by simp
-    with x semi have "(s' +|f x) \<in> err (opt A)" by (fast intro: closedD)
+    with x semi have "(s' +|f x) \<in> err (opt A)"
+      by (fast intro: semilat.closedI closedD)
     with x have "?if' \<in> err (opt A)" by auto
     hence "?P ls ?if'" by (rule IH) thus ?thesis by simp
   qed
   also have "\<dots> = ?if (l#ls) x"
     proof (cases "\<forall>(pc', s')\<in>set (l#ls). pc' \<noteq> pc + 1 \<longrightarrow> s' \<le>|r OK (cert ! pc')")