src/HOL/MicroJava/JVM/JVMExceptions.thy

 (*  Title:      HOL/MicroJava/JVM/JVMExceptions.thy
     Author:     Gerwin Klein, Martin Strecker
     Copyright   2001 Technische Universitaet Muenchen
 *)
 
-header {* \isaheader{Exception handling in the JVM} *}
+section {* Exception handling in the JVM *}
 
 theory JVMExceptions imports JVMInstructions begin
 
 definition match_exception_entry :: "jvm_prog \<Rightarrow> cname \<Rightarrow> p_count \<Rightarrow> exception_entry \<Rightarrow> bool" where
   "match_exception_entry G cn pc ee ==