src/HOL/MicroJava/JVM/JVMExceptions.thy
changeset 12911 704713ca07ea
parent 12545 7319d384d0d3
child 13052 3bf41c474a88
equal deleted inserted replaced
12910:f5bceeec9d91 12911:704713ca07ea
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Gerwin Klein, Martin Strecker
     3     Author:     Gerwin Klein, Martin Strecker
     4     Copyright   2001 Technische Universitaet Muenchen
     4     Copyright   2001 Technische Universitaet Muenchen
     5 *)
     5 *)
     6 
     6 
     7 header {* Exception handling in the JVM *}
     7 header {* \isaheader{Exception handling in the JVM} *}
     8 
     8 
     9 theory JVMExceptions = JVMInstructions:
     9 theory JVMExceptions = JVMInstructions:
    10 
    10 
    11 constdefs
    11 constdefs
    12   match_exception_entry :: "jvm_prog \<Rightarrow> cname \<Rightarrow> p_count \<Rightarrow> exception_entry \<Rightarrow> bool"
    12   match_exception_entry :: "jvm_prog \<Rightarrow> cname \<Rightarrow> p_count \<Rightarrow> exception_entry \<Rightarrow> bool"