equal
deleted
inserted
replaced
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 |