src/HOL/MicroJava/BV/BVExample.thy

   apply (unfold JVMType.sup_def JVMType.sl_def Opt.esl_def Err.sl_def
          stk_esl_def reg_sl_def Product.esl_def  
          Listn.sl_def upto_esl_def JType.esl_def Err.esl_def) 
   by simp
 
-lemmas [code] = JType.sup_def [unfolded exec_lub_def] JVM_le_unfold
-lemmas [code] = lesub_def plussub_def
-
 lemmas [code] =
   JType.sup_def [unfolded exec_lub_def]
+  JVM_le_unfold
+  lesub_def
+  plussub_def
   wf_class_code
   widen.equation
   match_exception_entry_def
 
 definition test1 where