--- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
Copyright 2000 TUM
*)
-header {* \isaheader{The Typing Framework for the JVM}\label{sec:JVM} *}
+section {* The Typing Framework for the JVM \label{sec:JVM} *}
theory Typing_Framework_JVM
imports "../DFA/Abstract_BV" JVMType EffectMono BVSpec
@@ -17,7 +17,7 @@
"opt_states G maxs maxr \<equiv> opt (\<Union>{list n (types G) |n. n \<le> maxs} \<times> list maxr (err (types G)))"
-section {* Executability of @{term check_bounded} *}
+subsection {* Executability of @{term check_bounded} *}
primrec list_all'_rec :: "('a \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> bool"
where
@@ -46,7 +46,7 @@
by (simp add: list_all_iff check_bounded_def)
-section {* Connecting JVM and Framework *}
+subsection {* Connecting JVM and Framework *}
lemma check_bounded_is_bounded:
"check_bounded ins et \<Longrightarrow> bounded (\<lambda>pc. eff (ins!pc) G pc et) (length ins)"