--- a/src/HOL/MicroJava/BV/Altern.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/BV/Altern.thy Sun Nov 02 17:58:35 2014 +0100
@@ -2,7 +2,7 @@
Author: Martin Strecker
*)
-header {* Alternative definition of well-typing of bytecode, used in compiler type correctness proof *}
+section {* Alternative definition of well-typing of bytecode, used in compiler type correctness proof *}
theory Altern
imports BVSpec
--- a/src/HOL/MicroJava/BV/BVExample.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/BV/BVExample.thy Sun Nov 02 17:58:35 2014 +0100
@@ -2,7 +2,7 @@
Author: Gerwin Klein
*)
-header {* \isaheader{Example Welltypings}\label{sec:BVExample} *}
+section {* Example Welltypings \label{sec:BVExample} *}
theory BVExample
imports
@@ -19,7 +19,7 @@
execution is guaranteed.
*}
-section "Setup"
+subsection "Setup"
text {* Abbreviations for definitions we will have to use often in the
proofs below: *}
@@ -178,7 +178,7 @@
by (unfold intervall_def) arith
-section "Program structure"
+subsection "Program structure"
text {*
The program is structurally wellformed:
@@ -225,7 +225,7 @@
by (simp add: wf_prog_def ws_prog_def wf_cdecl_mrT_cdecl_mdecl E_def SystemClasses_def)
qed
-section "Welltypings"
+subsection "Welltypings"
text {*
We show welltypings of the methods @{term append_name} in class @{term list_name},
and @{term makelist_name} in class @{term test_name}:
@@ -385,7 +385,7 @@
done
-section "Conformance"
+subsection "Conformance"
text {* Execution of the program will be typesafe, because its
start state conforms to the welltyping: *}
@@ -397,7 +397,7 @@
done
-section "Example for code generation: inferring method types"
+subsection "Example for code generation: inferring method types"
definition test_kil :: "jvm_prog \<Rightarrow> cname \<Rightarrow> ty list \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow>
exception_table \<Rightarrow> instr list \<Rightarrow> JVMType.state list" where
--- a/src/HOL/MicroJava/BV/BVNoTypeError.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy Sun Nov 02 17:58:35 2014 +0100
@@ -2,7 +2,7 @@
Author: Gerwin Klein
*)
-header {* \isaheader{Welltyped Programs produce no Type Errors} *}
+section {* Welltyped Programs produce no Type Errors *}
theory BVNoTypeError
imports "../JVM/JVMDefensive" BVSpecTypeSafe
--- a/src/HOL/MicroJava/BV/BVSpec.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/BV/BVSpec.thy Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-header {* \isaheader{The Bytecode Verifier}\label{sec:BVSpec} *}
+section {* The Bytecode Verifier \label{sec:BVSpec} *}
theory BVSpec
imports Effect
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-header {* \isaheader{BV Type Safety Proof}\label{sec:BVSpecTypeSafe} *}
+section {* BV Type Safety Proof \label{sec:BVSpecTypeSafe} *}
theory BVSpecTypeSafe
imports Correct
@@ -14,7 +14,7 @@
verifier only admits type safe programs.
*}
-section {* Preliminaries *}
+subsection {* Preliminaries *}
text {*
Simp and intro setup for the type safety proof:
@@ -41,7 +41,7 @@
done
-section {* Exception Handling *}
+subsection {* Exception Handling *}
text {*
Exceptions don't touch anything except the stack:
@@ -582,7 +582,7 @@
-section {* Single Instructions *}
+subsection {* Single Instructions *}
text {*
In this section we look at each single (welltyped) instruction, and
@@ -1265,7 +1265,7 @@
apply (rule Throw_correct, assumption+)
done
-section {* Main *}
+subsection {* Main *}
lemma correct_state_impl_Some_method:
"G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>
--- a/src/HOL/MicroJava/BV/Correct.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/BV/Correct.thy Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-header {* \isaheader{BV Type Safety Invariant} *}
+section {* BV Type Safety Invariant *}
theory Correct
imports BVSpec "../JVM/JVMExec"
@@ -68,7 +68,7 @@
by (cases X) auto
-section {* approx-val *}
+subsection {* approx-val *}
lemma approx_val_Err [simp,intro!]:
"approx_val G hp x Err"
@@ -96,7 +96,7 @@
\<Longrightarrow> approx_val G hp v T'"
by (cases T') (auto simp add: sup_ty_opt_OK intro: conf_widen)
-section {* approx-loc *}
+subsection {* approx-loc *}
lemma approx_loc_Nil [simp,intro!]:
"approx_loc G hp [] []"
@@ -170,7 +170,7 @@
apply blast
done
-section {* approx-stk *}
+subsection {* approx-stk *}
lemma approx_stk_rev_lem:
"approx_stk G hp (rev s) (rev t) = approx_stk G hp s t"
@@ -221,7 +221,7 @@
apply (erule conf_widen, assumption+)
done
-section {* oconf *}
+subsection {* oconf *}
lemma oconf_field_update:
"\<lbrakk>map_of (fields (G, oT)) FD = Some T; G,hp\<turnstile>v::\<preceq>T; G,hp\<turnstile>(oT,fs)\<surd> \<rbrakk>
@@ -242,7 +242,7 @@
apply (fastforce intro: approx_val_heap_update)
done
-section {* hconf *}
+subsection {* hconf *}
lemma hconf_newref:
"\<lbrakk> hp oref = None; G\<turnstile>h hp\<surd>; G,hp\<turnstile>obj\<surd> \<rbrakk> \<Longrightarrow> G\<turnstile>h hp(oref\<mapsto>obj)\<surd>"
@@ -259,7 +259,7 @@
simp add: obj_ty_def)
done
-section {* preallocated *}
+subsection {* preallocated *}
lemma preallocated_field_update:
"\<lbrakk> map_of (fields (G, oT)) X = Some T; hp a = Some(oT,fs);
@@ -289,7 +289,7 @@
with alloc show ?thesis by (simp add: preallocated_def)
qed
-section {* correct-frames *}
+subsection {* correct-frames *}
lemmas [simp del] = fun_upd_apply
--- a/src/HOL/MicroJava/BV/Effect.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/BV/Effect.thy Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
Copyright 2000 Technische Universitaet Muenchen
*)
-header {* \isaheader{Effect of Instructions on the State Type} *}
+section {* Effect of Instructions on the State Type *}
theory Effect
imports JVMType "../JVM/JVMExceptions"
--- a/src/HOL/MicroJava/BV/EffectMono.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/BV/EffectMono.thy Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
Copyright 2000 Technische Universitaet Muenchen
*)
-header {* \isaheader{Monotonicity of eff and app} *}
+section {* Monotonicity of eff and app *}
theory EffectMono
imports Effect
--- a/src/HOL/MicroJava/BV/JType.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/BV/JType.thy Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
Copyright 2000 TUM
*)
-header {* \isaheader{The Java Type System as Semilattice} *}
+section {* The Java Type System as Semilattice *}
theory JType
imports "../DFA/Semilattices" "../J/WellForm"
--- a/src/HOL/MicroJava/BV/JVM.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/BV/JVM.thy Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
Copyright 2000 TUM
*)
-header {* \isaheader{Kildall for the JVM}\label{sec:JVM} *}
+section {* Kildall for the JVM \label{sec:JVM} *}
theory JVM
imports Typing_Framework_JVM
--- a/src/HOL/MicroJava/BV/JVMType.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/BV/JVMType.thy Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
Copyright 2000 TUM
*)
-header {* \isaheader{The JVM Type System as Semilattice} *}
+section {* The JVM Type System as Semilattice *}
theory JVMType
imports JType
--- a/src/HOL/MicroJava/BV/LBVJVM.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/BV/LBVJVM.thy Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
Copyright 2000 TUM
*)
-header {* \isaheader{LBV for the JVM}\label{sec:JVM} *}
+section {* LBV for the JVM \label{sec:JVM} *}
theory LBVJVM
imports Typing_Framework_JVM
--- 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)"
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Sun Nov 02 17:58:35 2014 +0100
@@ -37,7 +37,7 @@
(********************************************************************************)
-section "index"
+subsection "index"
lemma local_env_snd: "
snd (local_env G C (mn, pTs) pns lvars) = map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class C)"
@@ -195,7 +195,7 @@
(********************************************************************************)
-section "Preservation of ST and LT by compTpExpr / compTpStmt"
+subsection "Preservation of ST and LT by compTpExpr / compTpStmt"
lemma sttp_of_comb_nil [simp]: "sttp_of (comb_nil sttp) = sttp"
by (simp add: comb_nil_def)
@@ -787,7 +787,7 @@
(* ********************************************************************** *)
-section "length of compExpr/ compTpExprs"
+subsection "length of compExpr/ compTpExprs"
(* ********************************************************************** *)
lemma length_comb [simp]: "length (mt_of ((f1 \<box> f2) sttp)) =
@@ -853,7 +853,7 @@
(* ********************************************************************** *)
-section "Correspondence bytecode - method types"
+subsection "Correspondence bytecode - method types"
(* ********************************************************************** *)
abbreviation (input)
@@ -2559,7 +2559,7 @@
(* ---------------------------------------------------------------------- *)
-section "Main Theorem"
+subsection "Main Theorem"
(* MAIN THEOREM:
Methodtype computed by comp is correct for bytecode generated by compTp *)
theorem wt_prog_comp: "wf_java_prog G \<Longrightarrow> wt_jvm_prog (comp G) (compTp G)"
--- a/src/HOL/MicroJava/DFA/Abstract_BV.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/DFA/Abstract_BV.thy Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
Copyright 2003 TUM
*)
-header {* Abstract Bytecode Verifier *}
+section {* Abstract Bytecode Verifier *}
(*<*)
theory Abstract_BV
--- a/src/HOL/MicroJava/DFA/Err.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/DFA/Err.thy Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
Copyright 2000 TUM
*)
-header {* \isaheader{The Error Type} *}
+section {* The Error Type *}
theory Err
imports Semilat
@@ -166,7 +166,7 @@
lemma Ok_in_err [iff]: "(OK x : err A) = (x:A)"
by (auto simp add: err_def)
-section {* lift *}
+subsection {* lift *}
lemma lift_in_errI:
"\<lbrakk> e : err S; !x:S. e = OK x \<longrightarrow> f x : err S \<rbrakk> \<Longrightarrow> lift f e : err S"
@@ -188,7 +188,7 @@
by (simp add: lift2_def plussub_def split: err.split)
-section {* sup *}
+subsection {* sup *}
lemma Err_sup_Err [simp]:
"Err +_(Err.sup f) x = Err"
@@ -217,7 +217,7 @@
apply (simp split: err.split)
done
-section {* semilat (err A) (le r) f *}
+subsection {* semilat (err A) (le r) f *}
lemma semilat_le_err_Err_plus [simp]:
"\<lbrakk> x: err A; semilat(err A, le r, f) \<rbrakk> \<Longrightarrow> Err +_f x = Err"
@@ -283,7 +283,7 @@
done
qed
-section {* semilat (err(Union AS)) *}
+subsection {* semilat (err(Union AS)) *}
(* FIXME? *)
lemma all_bex_swap_lemma [iff]:
--- a/src/HOL/MicroJava/DFA/Kildall.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/DFA/Kildall.thy Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
Copyright 2000 TUM
*)
-header {* \isaheader{Kildall's Algorithm}\label{sec:Kildall} *}
+section {* Kildall's Algorithm \label{sec:Kildall} *}
theory Kildall
imports SemilatAlg "~~/src/HOL/Library/While_Combinator"
--- a/src/HOL/MicroJava/DFA/LBVComplete.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/DFA/LBVComplete.thy Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
Copyright 2000 Technische Universitaet Muenchen
*)
-header {* \isaheader{Completeness of the LBV} *}
+section {* Completeness of the LBV *}
theory LBVComplete
imports LBVSpec Typing_Framework
--- a/src/HOL/MicroJava/DFA/LBVCorrect.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/DFA/LBVCorrect.thy Sun Nov 02 17:58:35 2014 +0100
@@ -2,7 +2,7 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-header {* \isaheader{Correctness of the LBV} *}
+section {* Correctness of the LBV *}
theory LBVCorrect
imports LBVSpec Typing_Framework
--- a/src/HOL/MicroJava/DFA/LBVSpec.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/DFA/LBVSpec.thy Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-header {* \isaheader{The Lightweight Bytecode Verifier} *}
+section {* The Lightweight Bytecode Verifier *}
theory LBVSpec
imports SemilatAlg Opt
@@ -92,7 +92,7 @@
declare Let_def [simp]
-section "more semilattice lemmas"
+subsection "more semilattice lemmas"
lemma (in lbv) sup_top [simp, elim]:
@@ -129,7 +129,7 @@
-section "merge"
+subsection "merge"
lemma (in lbv) merge_Nil [simp]:
"merge c pc [] x = x" by (simp add: mrg_def)
@@ -226,7 +226,7 @@
with x ss m show ?thesis by - (drule merge_def, auto split: split_if_asm)
qed
-section "wtl-inst-list"
+subsection "wtl-inst-list"
lemmas [iff] = not_Err_eq
@@ -301,7 +301,7 @@
with take pc show ?thesis by (auto simp add: min.absorb2)
qed
-section "preserves-type"
+subsection "preserves-type"
lemma (in lbv) merge_pres:
assumes s0: "snd`set ss \<subseteq> A" and x: "x \<in> A"
--- a/src/HOL/MicroJava/DFA/Listn.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/DFA/Listn.thy Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
Copyright 2000 TUM
*)
-header {* \isaheader{Fixed Length Lists} *}
+section {* Fixed Length Lists *}
theory Listn
imports Err
--- a/src/HOL/MicroJava/DFA/Opt.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/DFA/Opt.thy Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
Copyright 2000 TUM
*)
-header {* \isaheader{More about Options} *}
+section {* More about Options *}
theory Opt
imports Err
--- a/src/HOL/MicroJava/DFA/Product.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/DFA/Product.thy Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
Copyright 2000 TUM
*)
-header {* \isaheader{Products as Semilattices} *}
+section {* Products as Semilattices *}
theory Product
imports Err
--- a/src/HOL/MicroJava/DFA/Semilat.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/DFA/Semilat.thy Sun Nov 02 17:58:35 2014 +0100
@@ -3,10 +3,9 @@
Copyright 2000 TUM
*)
-header {*
- \chapter{Bytecode Verifier}\label{cha:bv}
- \isaheader{Semilattices}
-*}
+chapter {* Bytecode Verifier \label{cha:bv} *}
+
+section {* Semilattices *}
theory Semilat
imports Main "~~/src/HOL/Library/While_Combinator"
--- a/src/HOL/MicroJava/DFA/SemilatAlg.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/DFA/SemilatAlg.thy Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
Copyright 2002 Technische Universitaet Muenchen
*)
-header {* \isaheader{More on Semilattices} *}
+section {* More on Semilattices *}
theory SemilatAlg
imports Typing_Framework Product
--- a/src/HOL/MicroJava/DFA/Semilattices.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/DFA/Semilattices.thy Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
Copyright 2003 TUM
*)
-header {* Semilattices *}
+section {* Semilattices *}
(*<*)
theory Semilattices
--- a/src/HOL/MicroJava/DFA/Typing_Framework.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/DFA/Typing_Framework.thy Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
Copyright 2000 TUM
*)
-header {* \isaheader{Typing and Dataflow Analysis Framework} *}
+section {* Typing and Dataflow Analysis Framework *}
theory Typing_Framework
imports Listn
--- a/src/HOL/MicroJava/DFA/Typing_Framework_err.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/DFA/Typing_Framework_err.thy Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
Copyright 2000 TUM
*)
-header {* \isaheader{Lifting the Typing Framework to err, app, and eff} *}
+section {* Lifting the Typing Framework to err, app, and eff *}
theory Typing_Framework_err
imports Typing_Framework SemilatAlg
--- a/src/HOL/MicroJava/J/Conform.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/J/Conform.thy Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-header {* \isaheader{Conformity Relations for Type Soundness Proof} *}
+section {* Conformity Relations for Type Soundness Proof *}
theory Conform imports State WellType Exceptions begin
@@ -44,7 +44,7 @@
conforms ("_ ::\<preceq> _" [51,51] 50)
-section "hext"
+subsection "hext"
lemma hextI:
" \<forall>a C fs . h a = Some (C,fs) -->
@@ -79,7 +79,7 @@
done
-section "conf"
+subsection "conf"
lemma conf_Null [simp]: "G,h\<turnstile>Null::\<preceq>T = G\<turnstile>RefT NullT\<preceq>T"
apply (unfold conf_def)
@@ -182,7 +182,7 @@
done
-section "lconf"
+subsection "lconf"
lemma lconfD: "[| G,h\<turnstile>vs[::\<preceq>]Ts; Ts n = Some T |] ==> G,h\<turnstile>(the (vs n))::\<preceq>T"
apply (unfold lconf_def)
@@ -242,7 +242,7 @@
apply auto
done
-section "oconf"
+subsection "oconf"
lemma oconf_hext: "G,h\<turnstile>obj\<surd> ==> h\<le>|h' ==> G,h'\<turnstile>obj\<surd>"
apply (unfold oconf_def)
@@ -258,7 +258,7 @@
lemmas oconf_objD = oconf_obj [THEN iffD1, THEN spec, THEN spec, THEN mp]
-section "hconf"
+subsection "hconf"
lemma hconfD: "[|G\<turnstile>h h\<surd>; h a = Some obj|] ==> G,h\<turnstile>obj\<surd>"
apply (unfold hconf_def)
@@ -271,14 +271,14 @@
done
-section "xconf"
+subsection "xconf"
lemma xconf_raise_if: "xconf h x \<Longrightarrow> xconf h (raise_if b xcn x)"
by (simp add: xconf_def raise_if_def)
-section "conforms"
+subsection "conforms"
lemma conforms_heapD: "(x, (h, l))::\<preceq>(G, lT) ==> G\<turnstile>h h\<surd>"
apply (unfold conforms_def)
--- a/src/HOL/MicroJava/J/Decl.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/J/Decl.thy Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-header {* \isaheader{Class Declarations and Programs} *}
+section {* Class Declarations and Programs *}
theory Decl imports Type begin
--- a/src/HOL/MicroJava/J/Eval.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/J/Eval.thy Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-header {* \isaheader{Operational Evaluation (big step) Semantics} *}
+section {* Operational Evaluation (big step) Semantics *}
theory Eval imports State WellType begin
--- a/src/HOL/MicroJava/J/Example.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/J/Example.thy Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-header {* \isaheader{Example MicroJava Program} *}
+section {* Example MicroJava Program *}
theory Example imports SystemClasses Eval begin
--- a/src/HOL/MicroJava/J/JBasis.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/J/JBasis.thy Sun Nov 02 17:58:35 2014 +0100
@@ -2,16 +2,15 @@
Author: David von Oheimb, TU Muenchen
*)
-header {*
- \chapter{Java Source Language}\label{cha:j}
- \isaheader{Some Auxiliary Definitions}
-*}
+chapter {* Java Source Language \label{cha:j} *}
+
+section {* Some Auxiliary Definitions *}
theory JBasis imports Main "~~/src/HOL/Library/Transitive_Closure_Table" begin
lemmas [simp] = Let_def
-section "unique"
+subsection "unique"
definition unique :: "('a \<times> 'b) list => bool" where
"unique == distinct \<circ> map fst"
@@ -34,7 +33,7 @@
by (induct l) (auto dest: fst_in_set_lemma simp add: inj_eq)
-section "More about Maps"
+subsection "More about Maps"
lemma map_of_SomeI: "unique l ==> (k, x) : set l ==> map_of l k = Some x"
by (induct l) auto
--- a/src/HOL/MicroJava/J/JListExample.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/J/JListExample.thy Sun Nov 02 17:58:35 2014 +0100
@@ -2,7 +2,7 @@
Author: Stefan Berghofer
*)
-header {* \isaheader{Example for generating executable code from Java semantics} *}
+section {* Example for generating executable code from Java semantics *}
theory JListExample
imports Eval
--- a/src/HOL/MicroJava/J/JTypeSafe.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy Sun Nov 02 17:58:35 2014 +0100
@@ -2,7 +2,7 @@
Author: David von Oheimb, Technische Universitaet Muenchen
*)
-header {* \isaheader{Type Safety Proof} *}
+section {* Type Safety Proof *}
theory JTypeSafe imports Eval Conform begin
--- a/src/HOL/MicroJava/J/State.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/J/State.thy Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-header {* \isaheader{Program State} *}
+section {* Program State *}
theory State
imports TypeRel Value
--- a/src/HOL/MicroJava/J/SystemClasses.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/J/SystemClasses.thy Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
Copyright 2002 Technische Universitaet Muenchen
*)
-header {* \isaheader{System Classes} *}
+section {* System Classes *}
theory SystemClasses imports Decl begin
--- a/src/HOL/MicroJava/J/Term.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/J/Term.thy Sun Nov 02 17:58:35 2014 +0100
@@ -2,7 +2,7 @@
Author: David von Oheimb, Technische Universitaet Muenchen
*)
-header {* \isaheader{Expressions and Statements} *}
+section {* Expressions and Statements *}
theory Term imports Value begin
--- a/src/HOL/MicroJava/J/Type.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/J/Type.thy Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-header {* \isaheader{Java types} *}
+section {* Java types *}
theory Type imports JBasis begin
--- a/src/HOL/MicroJava/J/TypeRel.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/J/TypeRel.thy Sun Nov 02 17:58:35 2014 +0100
@@ -2,7 +2,7 @@
Author: David von Oheimb, Technische Universitaet Muenchen
*)
-header {* \isaheader{Relations between Java Types} *}
+section {* Relations between Java Types *}
theory TypeRel
imports Decl
--- a/src/HOL/MicroJava/J/Value.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/J/Value.thy Sun Nov 02 17:58:35 2014 +0100
@@ -2,7 +2,7 @@
Author: David von Oheimb, Technische Universitaet Muenchen
*)
-header {* \isaheader{Java Values} *}
+section {* Java Values *}
theory Value imports Type begin
--- a/src/HOL/MicroJava/J/WellForm.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/J/WellForm.thy Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-header {* \isaheader{Well-formedness of Java programs} *}
+section {* Well-formedness of Java programs *}
theory WellForm
imports TypeRel SystemClasses
--- a/src/HOL/MicroJava/J/WellType.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/J/WellType.thy Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-header {* \isaheader{Well-typedness Constraints} *}
+section {* Well-typedness Constraints *}
theory WellType imports Term WellForm begin
--- a/src/HOL/MicroJava/JVM/JVMDefensive.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/JVM/JVMDefensive.thy Sun Nov 02 17:58:35 2014 +0100
@@ -2,7 +2,7 @@
Author: Gerwin Klein
*)
-header {* \isaheader{A Defensive JVM} *}
+section {* A Defensive JVM *}
theory JVMDefensive
imports JVMExec
--- a/src/HOL/MicroJava/JVM/JVMExceptions.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExceptions.thy Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
Copyright 2001 Technische Universitaet Muenchen
*)
-header {* \isaheader{Exception handling in the JVM} *}
+section {* Exception handling in the JVM *}
theory JVMExceptions imports JVMInstructions begin
--- a/src/HOL/MicroJava/JVM/JVMExec.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExec.thy Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-header {* \isaheader{Program Execution in the JVM} *}
+section {* Program Execution in the JVM *}
theory JVMExec imports JVMExecInstr JVMExceptions begin
--- a/src/HOL/MicroJava/JVM/JVMExecInstr.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExecInstr.thy Sun Nov 02 17:58:35 2014 +0100
@@ -4,7 +4,7 @@
*)
-header {* \isaheader{JVM Instruction Semantics} *}
+section {* JVM Instruction Semantics *}
theory JVMExecInstr imports JVMInstructions JVMState begin
--- a/src/HOL/MicroJava/JVM/JVMInstructions.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/JVM/JVMInstructions.thy Sun Nov 02 17:58:35 2014 +0100
@@ -2,7 +2,7 @@
Author: Gerwin Klein, Technische Universitaet Muenchen
*)
-header {* \isaheader{Instructions of the JVM} *}
+section {* Instructions of the JVM *}
theory JVMInstructions imports JVMState begin
--- a/src/HOL/MicroJava/JVM/JVMListExample.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy Sun Nov 02 17:58:35 2014 +0100
@@ -2,7 +2,7 @@
Author: Stefan Berghofer
*)
-header {* \isaheader{Example for generating executable code from JVM semantics}\label{sec:JVMListExample} *}
+section {* Example for generating executable code from JVM semantics \label{sec:JVMListExample} *}
theory JVMListExample
imports "../J/SystemClasses" JVMExec
--- a/src/HOL/MicroJava/JVM/JVMState.thy Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/JVM/JVMState.thy Sun Nov 02 17:58:35 2014 +0100
@@ -2,16 +2,15 @@
Author: Cornelia Pusch, Gerwin Klein, Technische Universitaet Muenchen
*)
-header {*
- \chapter{Java Virtual Machine}\label{cha:jvm}
- \isaheader{State of the JVM}
-*}
+chapter {* Java Virtual Machine \label{cha:jvm} *}
+
+section {* State of the JVM *}
theory JVMState
imports "../J/Conform"
begin
-section {* Frame Stack *}
+subsection {* Frame Stack *}
type_synonym opstack = "val list"
type_synonym locvars = "val list"
type_synonym p_count = nat
@@ -30,16 +29,16 @@
-- "program counter within frame"
-section {* Exceptions *}
+subsection {* Exceptions *}
definition raise_system_xcpt :: "bool \<Rightarrow> xcpt \<Rightarrow> val option" where
"raise_system_xcpt b x \<equiv> raise_if b x None"
-section {* Runtime State *}
+subsection {* Runtime State *}
type_synonym
jvm_state = "val option \<times> aheap \<times> frame list" -- "exception flag, heap, frames"
-section {* Lemmas *}
+subsection {* Lemmas *}
lemma new_Addr_OutOfMemory:
"snd (new_Addr hp) = Some xcp \<Longrightarrow> xcp = Addr (XcptRef OutOfMemory)"
--- a/src/HOL/MicroJava/document/root.tex Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/document/root.tex Sun Nov 02 17:58:35 2014 +0100
@@ -10,10 +10,7 @@
\addtolength{\voffset}{-1cm}
\addtolength{\textheight}{2cm}
-\newcommand{\isaheader}[1]
-{\newpage\markright{Theory~\isabellecontext}\section{#1}}
-\renewcommand{\isamarkupheader}[1]{#1}
-\renewcommand{\isamarkupsection}[1]{\subsection{#1}}
+\renewcommand{\setisabellecontext}[1]{\markright{Theory~#1}}
\newcommand{\mJava}{$\mu$Java}
\newcommand{\secref}[1]{Section~\ref{#1}}