src/HOL/MicroJava/BV/JVM.thy
changeset 33954 1bc3b688548c
parent 33639 603320b93668
child 35416 d8d7d1b785af
     1.1 --- a/src/HOL/MicroJava/BV/JVM.thy	Wed Dec 02 12:04:07 2009 +0100
     1.2 +++ b/src/HOL/MicroJava/BV/JVM.thy	Tue Nov 24 14:37:23 2009 +0100
     1.3 @@ -5,8 +5,9 @@
     1.4  
     1.5  header {* \isaheader{Kildall for the JVM}\label{sec:JVM} *}
     1.6  
     1.7 -theory JVM imports Kildall Typing_Framework_JVM begin
     1.8 -
     1.9 +theory JVM
    1.10 +imports Typing_Framework_JVM
    1.11 +begin
    1.12  
    1.13  constdefs
    1.14    kiljvm :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow> 
    1.15 @@ -39,7 +40,7 @@
    1.16           simp add: symmetric sl_triple_conv)
    1.17        apply (simp (no_asm) add: JVM_le_unfold)
    1.18        apply (blast intro!: order_widen wf_converse_subcls1_impl_acc_subtype
    1.19 -                   dest: wf_subcls1 wfP_acyclicP wf_prog_ws_prog)
    1.20 +                   dest: wf_subcls1 wf_acyclic wf_prog_ws_prog)
    1.21       apply (simp add: JVM_le_unfold)
    1.22      apply (erule exec_pres_type)
    1.23     apply assumption