diff -r 75b2edff1af3 -r 4b1edf2f6bd2 src/HOL/MicroJava/BV/Opt.thy
--- a/src/HOL/MicroJava/BV/Opt.thy	Mon Mar 18 11:47:03 2002 +0100
+++ b/src/HOL/MicroJava/BV/Opt.thy	Wed Mar 20 13:21:07 2002 +0100
@@ -101,7 +101,7 @@
 done 
 
 
-lemma semilat_opt:
+lemma semilat_opt [intro, simp]:
   "\<And>L. err_semilat L \<Longrightarrow> err_semilat (Opt.esl L)"
 proof (unfold Opt.esl_def Err.sl_def, simp add: split_tupled_all)