src/HOL/MicroJava/BV/BVExample.thy
changeset 82774 2865a6618cba
parent 82664 e9f3b94eb6a0
equal deleted inserted replaced
82773:4ec8e654112f 82774:2865a6618cba
   463   apply (unfold JVMType.sup_def JVMType.sl_def Opt.esl_def Err.sl_def
   463   apply (unfold JVMType.sup_def JVMType.sl_def Opt.esl_def Err.sl_def
   464          stk_esl_def reg_sl_def Product.esl_def  
   464          stk_esl_def reg_sl_def Product.esl_def  
   465          Listn.sl_def upto_esl_def JType.esl_def Err.esl_def) 
   465          Listn.sl_def upto_esl_def JType.esl_def Err.esl_def) 
   466   by simp
   466   by simp
   467 
   467 
   468 lemmas [code] = JType.sup_def [unfolded exec_lub_def] JVM_le_unfold
       
   469 lemmas [code] = lesub_def plussub_def
       
   470 
       
   471 lemmas [code] =
   468 lemmas [code] =
   472   JType.sup_def [unfolded exec_lub_def]
   469   JType.sup_def [unfolded exec_lub_def]
       
   470   JVM_le_unfold
       
   471   lesub_def
       
   472   plussub_def
   473   wf_class_code
   473   wf_class_code
   474   widen.equation
   474   widen.equation
   475   match_exception_entry_def
   475   match_exception_entry_def
   476 
   476 
   477 definition test1 where
   477 definition test1 where