equal
deleted
inserted
replaced
308 |
308 |
309 theorem jvm_lbv_complete: |
309 theorem jvm_lbv_complete: |
310 "wt_jvm_prog G Phi \<Longrightarrow> wt_jvm_prog_lbv G (prg_cert G Phi)" |
310 "wt_jvm_prog G Phi \<Longrightarrow> wt_jvm_prog_lbv G (prg_cert G Phi)" |
311 apply (unfold wt_jvm_prog_def wt_jvm_prog_lbv_def) |
311 apply (unfold wt_jvm_prog_def wt_jvm_prog_lbv_def) |
312 apply (erule jvm_prog_lift) |
312 apply (erule jvm_prog_lift) |
313 apply (auto simp add: prg_cert_def intro wt_method_wt_lbv) |
313 apply (auto simp add: prg_cert_def intro: wt_method_wt_lbv) |
314 done |
314 done |
315 |
315 |
316 end |
316 end |