# HG changeset patch
# User wenzelm
# Date 1444253329 -7200
# Node ID 8b5f00202e1a34b45c3291e77dbd74c7f889d691
# Parent  a273bdac09345f2d8d6111746587e9ef5ade47e0
isabelle update_cartouches;

diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/BV/Altern.thy
--- a/src/HOL/MicroJava/BV/Altern.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/BV/Altern.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -2,7 +2,7 @@
     Author:     Martin Strecker
 *)
 
-section {* Alternative definition of well-typing of bytecode,  used in compiler type correctness proof *}
+section \<open>Alternative definition of well-typing of bytecode,  used in compiler type correctness proof\<close>
 
 theory Altern
 imports BVSpec
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/BV/BVExample.thy
--- a/src/HOL/MicroJava/BV/BVExample.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -2,7 +2,7 @@
     Author:     Gerwin Klein
 *)
 
-section {* Example Welltypings \label{sec:BVExample} *}
+section \<open>Example Welltypings \label{sec:BVExample}\<close>
 
 theory BVExample
 imports
@@ -11,26 +11,26 @@
   JVM
 begin
 
-text {*
+text \<open>
   This theory shows type correctness of the example program in section 
   \ref{sec:JVMListExample} (p. \pageref{sec:JVMListExample}) by
   explicitly providing a welltyping. It also shows that the start
   state of the program conforms to the welltyping; hence type safe
   execution is guaranteed.
-*}
+\<close>
 
 subsection "Setup"
 
-text {* Abbreviations for definitions we will have to use often in the
-proofs below: *}
+text \<open>Abbreviations for definitions we will have to use often in the
+proofs below:\<close>
 lemmas name_defs   = list_name_def test_name_def val_name_def next_name_def 
 lemmas system_defs = SystemClasses_def ObjectC_def NullPointerC_def 
                      OutOfMemoryC_def ClassCastC_def
 lemmas class_defs  = list_class_def test_class_def
 
-text {* These auxiliary proofs are for efficiency: class lookup,
+text \<open>These auxiliary proofs are for efficiency: class lookup,
 subclass relation, method and field lookup are computed only once:
-*}
+\<close>
 lemma class_Object [simp]:
   "class E Object = Some (undefined, [],[])"
   by (simp add: class_def system_defs E_def)
@@ -60,7 +60,7 @@
                         Xcpt ClassCast, Xcpt OutOfMemory, Object}"
   by (auto simp add: is_class_def class_def system_defs E_def name_defs class_defs)
 
-text {* The subclass releation spelled out: *}
+text \<open>The subclass releation spelled out:\<close>
 lemma subcls1:
   "subcls1 E = {(list_name,Object), (test_name,Object), (Xcpt NullPointer, Object),
                 (Xcpt ClassCast, Object), (Xcpt OutOfMemory, Object)}"
@@ -70,7 +70,7 @@
 apply auto
 done
 
-text {* The subclass relation is acyclic; hence its converse is well founded: *}
+text \<open>The subclass relation is acyclic; hence its converse is well founded:\<close>
 lemma notin_rtrancl:
   "(a, b) \<in> r\<^sup>* \<Longrightarrow> a \<noteq> b \<Longrightarrow> (\<And>y. (a, y) \<notin> r) \<Longrightarrow> False"
   by (auto elim: converse_rtranclE)
@@ -88,7 +88,7 @@
   apply (rule acyclic_subcls1_E)
   done  
 
-text {* Method and field lookup: *}
+text \<open>Method and field lookup:\<close>
 lemma method_Object [simp]:
   "method (E, Object) = Map.empty"
   by (simp add: method_rec_lemma [OF class_Object wf_subcls1_E])
@@ -150,7 +150,7 @@
 
 lemmas [simp] = is_class_def
 
-text {*
+text \<open>
   The next definition and three proof rules implement an algorithm to
   enumarate natural numbers. The command @{text "apply (elim pc_end pc_next pc_0"} 
   transforms a goal of the form
@@ -162,7 +162,7 @@
   @{text "\<dots>"}
 
   @{prop [display] "P n"} 
-*}
+\<close>
 definition intervall :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" ("_ \<in> [_, _')") where
   "x \<in> [a, b) \<equiv> a \<le> x \<and> x < b"
 
@@ -180,9 +180,9 @@
 
 subsection "Program structure"
 
-text {*
+text \<open>
   The program is structurally wellformed:
-*}
+\<close>
 
 lemma wf_struct:
   "wf_prog (\<lambda>G C mb. True) E" (is "wf_prog ?mb E")
@@ -226,10 +226,10 @@
 qed
 
 subsection "Welltypings"
-text {*
+text \<open>
   We show welltypings of the methods @{term append_name} in class @{term list_name}, 
   and @{term makelist_name} in class @{term test_name}:
-*}
+\<close>
 lemmas eff_simps [simp] = eff_def norm_eff_def xcpt_eff_def
 declare appInvoke [simp del]
 
@@ -289,7 +289,7 @@
   apply simp
   done
 
-text {* Some abbreviations for readability *} 
+text \<open>Some abbreviations for readability\<close> 
 abbreviation Clist :: ty 
   where "Clist == Class list_name"
 abbreviation Ctest :: ty
@@ -368,7 +368,7 @@
   apply simp
   done
 
-text {* The whole program is welltyped: *}
+text \<open>The whole program is welltyped:\<close>
 definition Phi :: prog_type ("\<Phi>") where
   "\<Phi> C sg \<equiv> if C = test_name \<and> sg = (makelist_name, []) then \<phi>\<^sub>m else          
              if C = list_name \<and> sg = (append_name, [Class list_name]) then \<phi>\<^sub>a else []"
@@ -386,8 +386,8 @@
 
 
 subsection "Conformance"
-text {* Execution of the program will be typesafe, because its
-  start state conforms to the welltyping: *}
+text \<open>Execution of the program will be typesafe, because its
+  start state conforms to the welltyping:\<close>
 
 lemma "E,\<Phi> \<turnstile>JVM start_state E test_name makelist_name \<surd>"
   apply (rule BV_correct_initial)
@@ -437,7 +437,7 @@
 code_printing
   constant some_elem \<rightharpoonup> (SML) "(case/ _ of/ Set/ xs/ =>/ hd/ xs)"
 
-text {* This code setup is just a demonstration and \emph{not} sound! *}
+text \<open>This code setup is just a demonstration and \emph{not} sound!\<close>
 
 lemma False
 proof -
@@ -480,10 +480,10 @@
 definition test2 where
   "test2 = test_kil E test_name [] (PrimT Void) 3 2 [] make_list_ins"
 
-ML_val {* 
+ML_val \<open>
   @{code test1}; 
   @{code test2};
-*}
+\<close>
 
 end
 
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/BV/BVNoTypeError.thy
--- a/src/HOL/MicroJava/BV/BVNoTypeError.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -2,16 +2,16 @@
     Author:     Gerwin Klein
 *)
 
-section {* Welltyped Programs produce no Type Errors *}
+section \<open>Welltyped Programs produce no Type Errors\<close>
 
 theory BVNoTypeError
 imports "../JVM/JVMDefensive" BVSpecTypeSafe
 begin
 
-text {*
+text \<open>
   Some simple lemmas about the type testing functions of the
   defensive JVM:
-*}
+\<close>
 lemma typeof_NoneD [simp,dest]:
   "typeof (\<lambda>v. None) v = Some x \<Longrightarrow> \<not>isAddr v"
   by (cases v) auto
@@ -217,10 +217,10 @@
   done
 
 
-text {*
+text \<open>
   The main theorem: welltyped programs do not produce type errors if they
   are started in a conformant state.
-*}
+\<close>
 theorem no_type_error:
   assumes welltyped: "wt_jvm_prog G Phi" and conforms: "G,Phi \<turnstile>JVM s \<surd>"
   shows "exec_d G (Normal s) \<noteq> TypeError"
@@ -391,11 +391,11 @@
 qed
 
 
-text {*
+text \<open>
   The theorem above tells us that, in welltyped programs, the
   defensive machine reaches the same result as the aggressive
   one (after arbitrarily many steps).
-*}
+\<close>
 theorem welltyped_aggressive_imp_defensive:
   "wt_jvm_prog G Phi \<Longrightarrow> G,Phi \<turnstile>JVM s \<surd> \<Longrightarrow> G \<turnstile> s \<midarrow>jvm\<rightarrow> t 
   \<Longrightarrow> G \<turnstile> (Normal s) \<midarrow>jvmd\<rightarrow> (Normal t)"
@@ -441,11 +441,11 @@
   from wt this s show ?thesis by (rule no_type_errors)
 qed
 
-text {*
+text \<open>
   As corollary we get that the aggressive and the defensive machine
   are equivalent for welltyped programs (if started in a conformant
   state or in the canonical start state)
-*} 
+\<close> 
 corollary welltyped_commutes:
   fixes G ("\<Gamma>") and Phi ("\<Phi>")
   assumes wt: "wt_jvm_prog \<Gamma> \<Phi>" and *: "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>" 
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/BV/BVSpec.thy
--- a/src/HOL/MicroJava/BV/BVSpec.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/BV/BVSpec.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -3,17 +3,17 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-section {* The Bytecode Verifier \label{sec:BVSpec} *}
+section \<open>The Bytecode Verifier \label{sec:BVSpec}\<close>
 
 theory BVSpec
 imports Effect
 begin
 
-text {*
+text \<open>
   This theory contains a specification of the BV. The specification
   describes correct typings of method bodies; it corresponds 
   to type \emph{checking}.
-*}
+\<close>
 
 definition
   -- "The program counter will always be inside the method:"
@@ -37,7 +37,7 @@
   (\<forall>(pc',s') \<in> set (eff i G pc et (phi!pc)). pc' < max_pc \<and> G \<turnstile> s' <=' phi!pc')"
 
 definition
-  -- {* The type at @{text "pc=0"} conforms to the method calling convention: *}
+  -- \<open>The type at @{text "pc=0"} conforms to the method calling convention:\<close>
   wt_start :: "[jvm_prog,cname,ty list,nat,method_type] \<Rightarrow> bool" where
   "wt_start G C pTs mxl phi \<longleftrightarrow>
   G \<turnstile> Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)) <=' phi!0"
@@ -96,10 +96,10 @@
   by (unfold wt_jvm_prog_def, drule method_wf_mdecl, 
       simp, simp, simp add: wf_mdecl_def wt_method_def)
 
-text {*
+text \<open>
   We could leave out the check @{term "pc' < max_pc"} in the 
   definition of @{term wt_instr} in the context of @{term wt_method}.
-*}
+\<close>
 lemma wt_instr_def2:
   "\<lbrakk> wt_jvm_prog G Phi; is_class G C;
       method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); pc < length ins; 
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -3,22 +3,22 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-section {* BV Type Safety Proof \label{sec:BVSpecTypeSafe} *}
+section \<open>BV Type Safety Proof \label{sec:BVSpecTypeSafe}\<close>
 
 theory BVSpecTypeSafe
 imports Correct
 begin
 
-text {*
+text \<open>
   This theory contains proof that the specification of the bytecode
   verifier only admits type safe programs.  
-*}
+\<close>
 
-subsection {* Preliminaries *}
+subsection \<open>Preliminaries\<close>
 
-text {*
+text \<open>
   Simp and intro setup for the type safety proof:
-*}
+\<close>
 lemmas defs1 = sup_state_conv correct_state_def correct_frame_def 
                wt_instr_def eff_def norm_eff_def 
 
@@ -27,10 +27,10 @@
 lemmas [simp del] = split_paired_All
 
 
-text {*
+text \<open>
   If we have a welltyped program and a conforming state, we
   can directly infer that the current instruction is well typed:
-*}
+\<close>
 lemma wt_jvm_prog_impl_wt_instr_cor:
   "\<lbrakk> wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
       G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
@@ -41,11 +41,11 @@
 done
 
 
-subsection {* Exception Handling *}
+subsection \<open>Exception Handling\<close>
 
-text {*
+text \<open>
   Exceptions don't touch anything except the stack:
-*}
+\<close>
 lemma exec_instr_xcpt:
   "(fst (exec_instr i G hp stk vars Cl sig pc frs) = Some xcp)
   = (\<exists>stk'. exec_instr i G hp stk vars Cl sig pc frs = 
@@ -53,10 +53,10 @@
   by (cases i, auto simp add: split_beta split: split_if_asm)
 
 
-text {*
+text \<open>
   Relates @{text match_any} from the Bytecode Verifier with 
   @{text match_exception_table} from the operational semantics:
-*}
+\<close>
 lemma in_match_any:
   "match_exception_table G xcpt pc et = Some pc' \<Longrightarrow> 
   \<exists>C. C \<in> set (match_any G pc et) \<and> G \<turnstile> xcpt \<preceq>C C \<and> 
@@ -123,14 +123,14 @@
   apply (auto split: split_if_asm)
   done
 
-text {*
+text \<open>
   We can prove separately that the recursive search for exception
   handlers (@{text find_handler}) in the frame stack results in 
   a conforming state (if there was no matching exception handler 
   in the current frame). We require that the exception is a valid
   heap address, and that the state before the exception occured
   conforms. 
-*}
+\<close>
 lemma uncaught_xcpt_correct:
   "\<And>f. \<lbrakk> wt_jvm_prog G phi; xcp = Addr adr; hp adr = Some T;
       G,phi \<turnstile>JVM (None, hp, f#frs)\<surd> \<rbrakk>
@@ -244,11 +244,11 @@
 qed
 
 declare raise_if_def [simp]
-text {*
+text \<open>
   The requirement of lemma @{text uncaught_xcpt_correct} (that
   the exception is a valid reference on the heap) is always met
   for welltyped instructions and conformant states:
-*}
+\<close>
 lemma exec_instr_xcpt_hp:
   "\<lbrakk>  fst (exec_instr (ins!pc) G hp stk vars Cl sig pc frs) = Some xcp;
        wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc;
@@ -280,10 +280,10 @@
   by (auto elim: preallocatedE [of hp x])
 
 
-text {*
+text \<open>
   Finally we can state that, whenever an exception occurs, the
   resulting next state always conforms:
-*}
+\<close>
 lemma xcpt_correct:
   "\<lbrakk> wt_jvm_prog G phi;
       method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
@@ -582,14 +582,14 @@
 
 
 
-subsection {* Single Instructions *}
+subsection \<open>Single Instructions\<close>
 
-text {*
+text \<open>
   In this section we look at each single (welltyped) instruction, and
   prove that the state after execution of the instruction still conforms.
   Since we have already handled exceptions above, we can now assume, that
   on exception occurs for this (single step) execution.
-*}
+\<close>
 
 lemmas [iff] = not_Err_eq
 
@@ -1220,13 +1220,13 @@
   by simp
 
 
-text {*
+text \<open>
   The next theorem collects the results of the sections above,
   i.e.~exception handling and the execution step for each 
   instruction. It states type safety for single step execution:
   in welltyped programs, a conforming state is transformed
   into another conforming state when one instruction is executed.
-*}
+\<close>
 theorem instr_correct:
 "\<lbrakk> wt_jvm_prog G phi;
   method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
@@ -1265,7 +1265,7 @@
 apply (rule Throw_correct, assumption+)
 done
 
-subsection {* Main *}
+subsection \<open>Main\<close>
 
 lemma correct_state_impl_Some_method:
   "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> 
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/BV/Correct.thy
--- a/src/HOL/MicroJava/BV/Correct.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/BV/Correct.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-section {* BV Type Safety Invariant *}
+section \<open>BV Type Safety Invariant\<close>
 
 theory Correct
 imports BVSpec "../JVM/JVMExec"
@@ -64,7 +64,7 @@
   by (cases X) auto
 
 
-subsection {* approx-val *}
+subsection \<open>approx-val\<close>
 
 lemma approx_val_Err [simp,intro!]:
   "approx_val G hp x Err"
@@ -92,7 +92,7 @@
   \<Longrightarrow> approx_val G hp v T'"
   by (cases T') (auto simp add: sup_ty_opt_OK intro: conf_widen)
 
-subsection {* approx-loc *}
+subsection \<open>approx-loc\<close>
 
 lemma approx_loc_Nil [simp,intro!]:
   "approx_loc G hp [] []"
@@ -166,7 +166,7 @@
   apply blast
   done
 
-subsection {* approx-stk *}
+subsection \<open>approx-stk\<close>
 
 lemma approx_stk_rev_lem:
   "approx_stk G hp (rev s) (rev t) = approx_stk G hp s t"
@@ -217,7 +217,7 @@
 apply (erule conf_widen, assumption+)
 done
 
-subsection {* oconf *}
+subsection \<open>oconf\<close>
 
 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>
@@ -238,7 +238,7 @@
   apply (fastforce intro: approx_val_heap_update)
   done
 
-subsection {* hconf *}
+subsection \<open>hconf\<close>
 
 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>"
@@ -255,7 +255,7 @@
                   simp add: obj_ty_def)
   done
 
-subsection {* preallocated *}
+subsection \<open>preallocated\<close>
 
 lemma preallocated_field_update:
   "\<lbrakk> map_of (fields (G, oT)) X = Some T; hp a = Some(oT,fs); 
@@ -285,7 +285,7 @@
   with alloc show ?thesis by (simp add: preallocated_def)
 qed
   
-subsection {* correct-frames *}
+subsection \<open>correct-frames\<close>
 
 lemmas [simp del] = fun_upd_apply
 
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/BV/Effect.thy
--- a/src/HOL/MicroJava/BV/Effect.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/BV/Effect.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
     Copyright   2000 Technische Universitaet Muenchen
 *)
 
-section {* Effect of Instructions on the State Type *}
+section \<open>Effect of Instructions on the State Type\<close>
 
 theory Effect 
 imports JVMType "../JVM/JVMExceptions"
@@ -11,7 +11,7 @@
 
 type_synonym succ_type = "(p_count \<times> state_type option) list"
 
-text {* Program counter of successor instructions: *}
+text \<open>Program counter of successor instructions:\<close>
 primrec succs :: "instr \<Rightarrow> p_count \<Rightarrow> p_count list" where
   "succs (Load idx) pc         = [pc+1]"
 | "succs (Store idx) pc        = [pc+1]"
@@ -226,10 +226,10 @@
 
 lemmas [simp] = app_def xcpt_app_def
 
-text {* 
+text \<open>
 \medskip
 simp rules for @{term app}
-*}
+\<close>
 lemma appNone[simp]: "app i G maxs rT pc et None = True" by simp
 
 
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/BV/EffectMono.thy
--- a/src/HOL/MicroJava/BV/EffectMono.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/BV/EffectMono.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
     Copyright   2000 Technische Universitaet Muenchen
 *)
 
-section {* Monotonicity of eff and app *}
+section \<open>Monotonicity of eff and app\<close>
 
 theory EffectMono
 imports Effect
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/BV/JType.thy
--- a/src/HOL/MicroJava/BV/JType.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/BV/JType.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
     Copyright   2000 TUM
 *)
 
-section {* The Java Type System as Semilattice *}
+section \<open>The Java Type System as Semilattice\<close>
 
 theory JType
 imports "../DFA/Semilattices" "../J/WellForm"
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/BV/JVM.thy
--- a/src/HOL/MicroJava/BV/JVM.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/BV/JVM.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
     Copyright   2000 TUM
 *)
 
-section {* Kildall for the JVM \label{sec:JVM} *}
+section \<open>Kildall for the JVM \label{sec:JVM}\<close>
 
 theory JVM
 imports Typing_Framework_JVM
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/BV/JVMType.thy
--- a/src/HOL/MicroJava/BV/JVMType.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/BV/JVMType.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
     Copyright   2000 TUM
 *)
 
-section {* The JVM Type System as Semilattice *}
+section \<open>The JVM Type System as Semilattice\<close>
 
 theory JVMType
 imports JType
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/BV/LBVJVM.thy
--- a/src/HOL/MicroJava/BV/LBVJVM.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/BV/LBVJVM.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
     Copyright   2000 TUM
 *)
 
-section {* LBV for the JVM \label{sec:JVM} *}
+section \<open>LBV for the JVM \label{sec:JVM}\<close>
 
 theory LBVJVM
 imports Typing_Framework_JVM
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/BV/Typing_Framework_JVM.thy
--- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
     Copyright   2000 TUM
 *)
 
-section {* The Typing Framework for the JVM \label{sec:JVM} *}
+section \<open>The Typing Framework for the JVM \label{sec:JVM}\<close>
 
 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)))"
 
 
-subsection {*  Executability of @{term check_bounded} *}
+subsection \<open>Executability of @{term check_bounded}\<close>
 
 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)
   
 
-subsection {* Connecting JVM and Framework *}
+subsection \<open>Connecting JVM and Framework\<close>
 
 lemma check_bounded_is_bounded:
   "check_bounded ins et \<Longrightarrow> bounded (\<lambda>pc. eff (ins!pc) G pc et) (length ins)"  
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/Comp/CorrCompTp.thy
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -1276,7 +1276,7 @@
     apply assumption
    apply (simp add: max_ssize_def max_of_list_elem ssize_sto_def)
 
-  -- {* @{text "<=s"} *}
+  -- \<open>@{text "<=s"}\<close>
   apply (frule max_spec2mheads, (erule exE)+, (erule conjE)+)
   apply (simp add: wf_prog_ws_prog [THEN comp_method])
   apply (simp add: max_spec_preserves_length [symmetric])
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/DFA/Abstract_BV.thy
--- a/src/HOL/MicroJava/DFA/Abstract_BV.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/DFA/Abstract_BV.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
     Copyright   2003 TUM
 *)
 
-section {* Abstract Bytecode Verifier *}
+section \<open>Abstract Bytecode Verifier\<close>
 
 (*<*)
 theory Abstract_BV
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/DFA/Err.thy
--- a/src/HOL/MicroJava/DFA/Err.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/DFA/Err.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
     Copyright   2000 TUM
 *)
 
-section {* The Error Type *}
+section \<open>The Error Type\<close>
 
 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)
 
-subsection {* lift *}
+subsection \<open>lift\<close>
 
 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)
 
 
-subsection {* sup *}
+subsection \<open>sup\<close>
 
 lemma Err_sup_Err [simp]:
   "Err +_(Err.sup f) x = Err"
@@ -217,7 +217,7 @@
 apply (simp split: err.split)
 done 
 
-subsection {* semilat (err A) (le r) f *}
+subsection \<open>semilat (err A) (le r) f\<close>
 
 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
 
-subsection {* semilat (err(Union AS)) *}
+subsection \<open>semilat (err(Union AS))\<close>
 
 (* FIXME? *)
 lemma all_bex_swap_lemma [iff]:
@@ -301,11 +301,11 @@
 apply fast
 done 
 
-text {* 
+text \<open>
   If @{term "AS = {}"} the thm collapses to
   @{prop "order r & closed {Err} f & Err +_f Err = Err"}
   which may not hold 
-*}
+\<close>
 lemma err_semilat_UnionI:
   "\<lbrakk> !A:AS. err_semilat(A, r, f); AS ~= {}; 
       !A:AS.!B:AS. A~=B \<longrightarrow> (!a:A.!b:B. ~ a <=_r b & a +_f b = Err) \<rbrakk> 
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/DFA/Kildall.thy
--- a/src/HOL/MicroJava/DFA/Kildall.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/DFA/Kildall.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
     Copyright   2000 TUM
 *)
 
-section {* Kildall's Algorithm \label{sec:Kildall} *}
+section \<open>Kildall's Algorithm \label{sec:Kildall}\<close>
 
 theory Kildall
 imports SemilatAlg "~~/src/HOL/Library/While_Combinator"
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/DFA/LBVComplete.thy
--- a/src/HOL/MicroJava/DFA/LBVComplete.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/DFA/LBVComplete.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
     Copyright   2000 Technische Universitaet Muenchen
 *)
 
-section {* Completeness of the LBV *}
+section \<open>Completeness of the LBV\<close>
 
 theory LBVComplete
 imports LBVSpec Typing_Framework
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/DFA/LBVCorrect.thy
--- a/src/HOL/MicroJava/DFA/LBVCorrect.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/DFA/LBVCorrect.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -2,7 +2,7 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-section {* Correctness of the LBV *}
+section \<open>Correctness of the LBV\<close>
 
 theory LBVCorrect
 imports LBVSpec Typing_Framework
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/DFA/LBVSpec.thy
--- a/src/HOL/MicroJava/DFA/LBVSpec.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/DFA/LBVSpec.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-section {* The Lightweight Bytecode Verifier *}
+section \<open>The Lightweight Bytecode Verifier\<close>
 
 theory LBVSpec
 imports SemilatAlg Opt
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/DFA/Listn.thy
--- a/src/HOL/MicroJava/DFA/Listn.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/DFA/Listn.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
     Copyright   2000 TUM
 *)
 
-section {* Fixed Length Lists *}
+section \<open>Fixed Length Lists\<close>
 
 theory Listn
 imports Err
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/DFA/Opt.thy
--- a/src/HOL/MicroJava/DFA/Opt.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/DFA/Opt.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
     Copyright   2000 TUM
 *)
 
-section {* More about Options *}
+section \<open>More about Options\<close>
 
 theory Opt
 imports Err
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/DFA/Product.thy
--- a/src/HOL/MicroJava/DFA/Product.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/DFA/Product.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
     Copyright   2000 TUM
 *)
 
-section {* Products as Semilattices *}
+section \<open>Products as Semilattices\<close>
 
 theory Product
 imports Err
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/DFA/Semilat.thy
--- a/src/HOL/MicroJava/DFA/Semilat.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/DFA/Semilat.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -3,9 +3,9 @@
     Copyright   2000 TUM
 *)
 
-chapter {* Bytecode Verifier \label{cha:bv} *}
+chapter \<open>Bytecode Verifier \label{cha:bv}\<close>
 
-section {* Semilattices *}
+section \<open>Semilattices\<close>
 
 theory Semilat
 imports Main "~~/src/HOL/Library/While_Combinator"
@@ -301,7 +301,7 @@
   \<Longrightarrow> is_lub (r^* ) x y (some_lub (r^* ) x y)"
   (*<*) by (fastforce dest: single_valued_has_lubs simp add: some_lub_conv) (*>*)
 
-subsection{*An executable lub-finder*}
+subsection\<open>An executable lub-finder\<close>
 
 definition exec_lub :: "('a * 'a) set \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a binop" where
 "exec_lub r f x y \<equiv> while (\<lambda>z. (x,z) \<notin> r\<^sup>*) f y"
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/DFA/SemilatAlg.thy
--- a/src/HOL/MicroJava/DFA/SemilatAlg.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/DFA/SemilatAlg.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
     Copyright   2002 Technische Universitaet Muenchen
 *)
 
-section {* More on Semilattices *}
+section \<open>More on Semilattices\<close>
 
 theory SemilatAlg
 imports Typing_Framework Product
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/DFA/Semilattices.thy
--- a/src/HOL/MicroJava/DFA/Semilattices.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/DFA/Semilattices.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
     Copyright   2003 TUM
 *)
 
-section {* Semilattices *}
+section \<open>Semilattices\<close>
 
 (*<*)
 theory Semilattices
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/DFA/Typing_Framework.thy
--- a/src/HOL/MicroJava/DFA/Typing_Framework.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/DFA/Typing_Framework.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -3,15 +3,15 @@
     Copyright   2000 TUM
 *)
 
-section {* Typing and Dataflow Analysis Framework *}
+section \<open>Typing and Dataflow Analysis Framework\<close>
 
 theory Typing_Framework
 imports Listn
 begin
 
-text {* 
+text \<open>
   The relationship between dataflow analysis and a welltyped-instruction predicate. 
-*}
+\<close>
 type_synonym 's step_type = "nat \<Rightarrow> 's \<Rightarrow> (nat \<times> 's) list"
 
 definition stable :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> nat \<Rightarrow> bool" where
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/DFA/Typing_Framework_err.thy
--- a/src/HOL/MicroJava/DFA/Typing_Framework_err.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/DFA/Typing_Framework_err.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
     Copyright   2000 TUM
 *)
 
-section {* Lifting the Typing Framework to err, app, and eff *}
+section \<open>Lifting the Typing Framework to err, app, and eff\<close>
 
 theory Typing_Framework_err
 imports Typing_Framework SemilatAlg
@@ -158,12 +158,12 @@
 
 
 
-text {*
+text \<open>
   There used to be a condition here that each instruction must have a
   successor. This is not needed any more, because the definition of
   @{term error} trivially ensures that there is a successor for
   the critical case where @{term app} does not hold. 
-*}
+\<close>
 lemma wt_err_imp_wt_app_eff:
   assumes wt: "wt_err_step r (err_step (size ts) app step) ts"
   assumes b:  "bounded (err_step (size ts) app step) (size ts)"
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/J/Conform.thy
--- a/src/HOL/MicroJava/J/Conform.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/J/Conform.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-section {* Conformity Relations for Type Soundness Proof *}
+section \<open>Conformity Relations for Type Soundness Proof\<close>
 
 theory Conform imports State WellType Exceptions begin
 
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/J/Decl.thy
--- a/src/HOL/MicroJava/J/Decl.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/J/Decl.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-section {* Class Declarations and Programs *}
+section \<open>Class Declarations and Programs\<close>
 
 theory Decl imports Type begin
 
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/J/Eval.thy
--- a/src/HOL/MicroJava/J/Eval.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/J/Eval.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-section {* Operational Evaluation (big step) Semantics *}
+section \<open>Operational Evaluation (big step) Semantics\<close>
 
 theory Eval imports State WellType begin
 
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/J/Example.thy
--- a/src/HOL/MicroJava/J/Example.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/J/Example.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -3,11 +3,11 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-section {* Example MicroJava Program *}
+section \<open>Example MicroJava Program\<close>
 
 theory Example imports SystemClasses Eval begin
 
-text {* 
+text \<open>
 The following example MicroJava program includes:
  class declarations with inheritance, hiding of fields, and overriding of
   methods (with refined result type), 
@@ -34,15 +34,15 @@
   }
 }
 \end{verbatim}
-*}
+\<close>
 
 datatype cnam' = Base' | Ext'
 datatype vnam' = vee' | x' | e'
 
-text {*
+text \<open>
   @{text cnam'} and @{text vnam'} are intended to be isomorphic 
   to @{text cnam} and @{text vnam}
-*}
+\<close>
 
 axiomatization cnam' :: "cnam' => cname"
 where
@@ -378,7 +378,7 @@
 apply (rule ty_expr_ty_exprs_wt_stmt.intros) -- ";;"
 apply  (rule t) -- "Expr"
 apply  (rule t) -- "LAss"
-apply    simp -- {* @{text "e \<noteq> This"} *}
+apply    simp -- \<open>@{text "e \<noteq> This"}\<close>
 apply    (rule t) -- "LAcc"
 apply     (simp (no_asm))
 apply    (simp (no_asm))
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/J/Exceptions.thy
--- a/src/HOL/MicroJava/J/Exceptions.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/J/Exceptions.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -5,7 +5,7 @@
 
 theory Exceptions imports State begin
 
-text {* a new, blank object with default values in all fields: *}
+text \<open>a new, blank object with default values in all fields:\<close>
 definition blank :: "'c prog \<Rightarrow> cname \<Rightarrow> obj" where
   "blank G C \<equiv> (C,init_vars (fields(G,C)))" 
 
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/J/JBasis.thy
--- a/src/HOL/MicroJava/J/JBasis.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/J/JBasis.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -2,9 +2,9 @@
     Author:     David von Oheimb, TU Muenchen
 *)
 
-chapter {* Java Source Language \label{cha:j} *}
+chapter \<open>Java Source Language \label{cha:j}\<close>
 
-section {* Some Auxiliary Definitions *}
+section \<open>Some Auxiliary Definitions\<close>
 
 theory JBasis imports Main "~~/src/HOL/Library/Transitive_Closure_Table" begin 
 
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/J/JListExample.thy
--- a/src/HOL/MicroJava/J/JListExample.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/J/JListExample.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -2,7 +2,7 @@
     Author:     Stefan Berghofer
 *)
 
-section {* Example for generating executable code from Java semantics *}
+section \<open>Example for generating executable code from Java semantics\<close>
 
 theory JListExample
 imports Eval
@@ -151,7 +151,7 @@
   "test = exec_i_i_i_o example_prg (Norm (empty, empty)) E"
 by(auto intro: exec_i_i_i_oI intro!: pred_eqI elim: exec_i_i_i_oE simp add: test_def)
 
-ML_val {* 
+ML_val \<open>
   val SOME ((_, (heap, locs)), _) = Predicate.yield @{code test};
   locs @{code l1_name};
   locs @{code l2_name};
@@ -177,6 +177,6 @@
 
   val_field (Suc (Suc (Suc @{code "0 :: nat"})));
   next_field (Suc (Suc (Suc @{code "0 :: nat"})));
-*}
+\<close>
 
 end
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/J/JTypeSafe.thy
--- a/src/HOL/MicroJava/J/JTypeSafe.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -2,7 +2,7 @@
     Author:     David von Oheimb, Technische Universitaet Muenchen
 *)
 
-section {* Type Safety Proof *}
+section \<open>Type Safety Proof\<close>
 
 theory JTypeSafe imports Eval Conform begin
 
@@ -176,12 +176,12 @@
 declare fun_upd_same [simp]
 declare wf_prog_ws_prog [simp]
 
-ML{*
+ML\<open>
 fun forward_hyp_tac ctxt =
   ALLGOALS (TRY o (EVERY' [dresolve_tac ctxt [spec], mp_tac ctxt,
     (mp_tac ctxt ORELSE' (dresolve_tac ctxt [spec] THEN' mp_tac ctxt)),
     REPEAT o (eresolve_tac ctxt [conjE])]))
-*}
+\<close>
 
 
 theorem eval_evals_exec_type_sound: 
@@ -201,8 +201,8 @@
 -- "several simplifications, XcptE, XcptEs, XcptS, Skip, Nil??"
 apply( simp_all)
 apply( tactic "ALLGOALS (REPEAT o resolve_tac @{context} [impI, allI])")
-apply( tactic {* ALLGOALS (eresolve_tac @{context} [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}]
-  THEN_ALL_NEW (full_simp_tac (put_simpset (simpset_of @{theory_context Conform}) @{context}))) *})
+apply( tactic \<open>ALLGOALS (eresolve_tac @{context} [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}]
+  THEN_ALL_NEW (full_simp_tac (put_simpset (simpset_of @{theory_context Conform}) @{context})))\<close>)
 apply(tactic "ALLGOALS (EVERY' [REPEAT o (eresolve_tac @{context} [conjE]), REPEAT o hyp_subst_tac @{context}])")
 
 -- "Level 7"
@@ -241,12 +241,12 @@
 apply( fast elim: conforms_localD [THEN lconfD])
 
 -- "for FAss"
-apply( tactic {* EVERY'[eresolve_tac @{context} [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}] 
-       THEN_ALL_NEW (full_simp_tac @{context}), REPEAT o (eresolve_tac @{context} [conjE]), hyp_subst_tac @{context}] 3*})
+apply( tactic \<open>EVERY'[eresolve_tac @{context} [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}] 
+       THEN_ALL_NEW (full_simp_tac @{context}), REPEAT o (eresolve_tac @{context} [conjE]), hyp_subst_tac @{context}] 3\<close>)
 
 -- "for if"
-apply( tactic {* (Induct_Tacs.case_tac @{context} "the_Bool v" [] NONE THEN_ALL_NEW
-  (asm_full_simp_tac @{context})) 7*})
+apply( tactic \<open>(Induct_Tacs.case_tac @{context} "the_Bool v" [] NONE THEN_ALL_NEW
+  (asm_full_simp_tac @{context})) 7\<close>)
 
 apply (tactic "forward_hyp_tac @{context}")
 
@@ -277,8 +277,8 @@
 
 -- "7 LAss"
 apply (fold fun_upd_def)
-apply( tactic {* (eresolve_tac @{context} [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}]
-                 THEN_ALL_NEW (full_simp_tac @{context})) 1 *})
+apply( tactic \<open>(eresolve_tac @{context} [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}]
+                 THEN_ALL_NEW (full_simp_tac @{context})) 1\<close>)
 apply (intro strip)
 apply (case_tac E)
 apply (simp)
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/J/State.thy
--- a/src/HOL/MicroJava/J/State.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/J/State.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-section {* Program State *}
+section \<open>Program State\<close>
 
 theory State
 imports TypeRel Value
@@ -21,7 +21,7 @@
 definition init_vars :: "('a \<times> ty) list => ('a \<rightharpoonup> val)" where
  "init_vars == map_of o map (\<lambda>(n,T). (n,default_val T))"
 
-type_synonym aheap = "loc \<rightharpoonup> obj"    -- {* "@{text heap}" used in a translation below *}
+type_synonym aheap = "loc \<rightharpoonup> obj"    -- \<open>"@{text heap}" used in a translation below\<close>
 type_synonym locals = "vname \<rightharpoonup> val"  -- "simple state, i.e. variable contents"
 
 type_synonym state = "aheap \<times> locals"      -- "heap, local parameter including This"
@@ -52,7 +52,7 @@
 definition raise_if :: "bool \<Rightarrow> xcpt \<Rightarrow> val option \<Rightarrow> val option" where
   "raise_if b x xo \<equiv> if b \<and>  (xo = None) then Some (Addr (XcptRef x)) else xo"
 
-text {* Make @{text new_Addr} completely specified (at least for the code generator) *}
+text \<open>Make @{text new_Addr} completely specified (at least for the code generator)\<close>
 (*
 definition new_Addr  :: "aheap => loc \<times> val option" where
   "new_Addr h \<equiv> SOME (a,x). (h a = None \<and>  x = None) |  x = Some (Addr (XcptRef OutOfMemory))"
@@ -154,7 +154,7 @@
 lemma c_hupd_fst [simp]: "fst (c_hupd h (x, s)) = x"
 by (simp add: c_hupd_def split_beta)
 
-text {* Naive implementation for @{term "new_Addr"} by exhaustive search *}
+text \<open>Naive implementation for @{term "new_Addr"} by exhaustive search\<close>
 
 definition gen_new_Addr :: "aheap => nat \<Rightarrow> loc \<times> val option" where
   "gen_new_Addr h n \<equiv> 
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/J/SystemClasses.thy
--- a/src/HOL/MicroJava/J/SystemClasses.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/J/SystemClasses.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -3,14 +3,14 @@
     Copyright   2002 Technische Universitaet Muenchen
 *)
 
-section {* System Classes *}
+section \<open>System Classes\<close>
 
 theory SystemClasses imports Decl begin
 
-text {*
+text \<open>
   This theory provides definitions for the @{text Object} class,
   and the system exceptions.
-*}
+\<close>
 
 definition ObjectC :: "'c cdecl" where
   [code_unfold]: "ObjectC \<equiv> (Object, (undefined,[],[]))"
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/J/Term.thy
--- a/src/HOL/MicroJava/J/Term.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/J/Term.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -2,7 +2,7 @@
     Author:     David von Oheimb, Technische Universitaet Muenchen
 *)
 
-section {* Expressions and Statements *}
+section \<open>Expressions and Statements\<close>
 
 theory Term imports Value begin
 
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/J/Type.thy
--- a/src/HOL/MicroJava/J/Type.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/J/Type.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-section {* Java types *}
+section \<open>Java types\<close>
 
 theory Type imports JBasis begin
 
@@ -17,7 +17,7 @@
 
 end
 
-text {* These instantiations only ensure that the merge in theory @{text "MicroJava"} succeeds. FIXME *}
+text \<open>These instantiations only ensure that the merge in theory @{text "MicroJava"} succeeds. FIXME\<close>
 
 instantiation cnam :: typerep
 begin
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/J/TypeRel.thy
--- a/src/HOL/MicroJava/J/TypeRel.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -2,7 +2,7 @@
     Author:     David von Oheimb, Technische Universitaet Muenchen
 *)
 
-section {* Relations between Java Types *}
+section \<open>Relations between Java Types\<close>
 
 theory TypeRel
 imports Decl
@@ -74,7 +74,7 @@
 
 
 
-text {* Code generator setup *}
+text \<open>Code generator setup\<close>
 
 code_pred 
   (modes: i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool, i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool)
@@ -134,10 +134,10 @@
     assume "(C, D, fs, ms) \<in> set G"
       and "C \<noteq> Object"
       and subcls: "G \<turnstile> fst (the (class G C)) \<preceq>C C"
-    from `(C, D, fs, ms) \<in> set G` obtain D' fs' ms'
+    from \<open>(C, D, fs, ms) \<in> set G\<close> obtain D' fs' ms'
       where "class": "class G C = Some (D', fs', ms')"
       unfolding class_def by(auto dest!: weak_map_of_SomeI)
-    hence "G \<turnstile> C \<prec>C1 D'" using `C \<noteq> Object` ..
+    hence "G \<turnstile> C \<prec>C1 D'" using \<open>C \<noteq> Object\<close> ..
     hence *: "(C, D') \<in> (subcls1 G)^+" ..
     also from * acyc have "C \<noteq> D'" by(auto simp add: acyclic_def)
     with subcls "class" have "(D', C) \<in> (subcls1 G)^+" by(auto dest: rtranclD)
@@ -154,20 +154,20 @@
       case base
       then obtain rest where "class G C = Some (C, rest)"
         and "C \<noteq> Object" by cases
-      from `class G C = Some (C, rest)` have "(C, C, rest) \<in> set G"
+      from \<open>class G C = Some (C, rest)\<close> have "(C, C, rest) \<in> set G"
         unfolding class_def by(rule map_of_SomeD)
-      with `C \<noteq> Object` `class G C = Some (C, rest)`
+      with \<open>C \<noteq> Object\<close> \<open>class G C = Some (C, rest)\<close>
       have "\<not> G \<turnstile> C \<preceq>C C" by(auto dest: rhs)
       thus False by simp
     next
       case (step D)
-      from `G \<turnstile> D \<prec>C1 C` obtain rest where "class G D = Some (C, rest)"
+      from \<open>G \<turnstile> D \<prec>C1 C\<close> obtain rest where "class G D = Some (C, rest)"
         and "D \<noteq> Object" by cases
-      from `class G D = Some (C, rest)` have "(D, C, rest) \<in> set G"
+      from \<open>class G D = Some (C, rest)\<close> have "(D, C, rest) \<in> set G"
         unfolding class_def by(rule map_of_SomeD)
-      with `D \<noteq> Object` `class G D = Some (C, rest)`
+      with \<open>D \<noteq> Object\<close> \<open>class G D = Some (C, rest)\<close>
       have "\<not> G \<turnstile> C \<preceq>C D" by(auto dest: rhs)
-      moreover from `(C, D) \<in> (subcls1 G)\<^sup>+`
+      moreover from \<open>(C, D) \<in> (subcls1 G)\<^sup>+\<close>
       have "G \<turnstile> C \<preceq>C D" by(rule trancl_into_rtrancl)
       ultimately show False by contradiction
     qed
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/J/Value.thy
--- a/src/HOL/MicroJava/J/Value.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/J/Value.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -2,7 +2,7 @@
     Author:     David von Oheimb, Technische Universitaet Muenchen
 *)
 
-section {* Java Values *}
+section \<open>Java Values\<close>
 
 theory Value imports Type begin
 
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/J/WellForm.thy
--- a/src/HOL/MicroJava/J/WellForm.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/J/WellForm.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -3,13 +3,13 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-section {* Well-formedness of Java programs *}
+section \<open>Well-formedness of Java programs\<close>
 
 theory WellForm
 imports TypeRel SystemClasses
 begin
 
-text {*
+text \<open>
 for static checks on expressions and statements, see WellType.
 
 \begin{description}
@@ -24,7 +24,7 @@
 \item for uniformity, Object is assumed to be declared like any other class
 \end{itemize}
 \end{description}
-*}
+\<close>
 type_synonym 'c wf_mb = "'c prog => cname => 'c mdecl => bool"
 
 definition wf_syscls :: "'c prog => bool" where
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/J/WellType.thy
--- a/src/HOL/MicroJava/J/WellType.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/J/WellType.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -3,11 +3,11 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-section {* Well-typedness Constraints *}
+section \<open>Well-typedness Constraints\<close>
 
 theory WellType imports Term WellForm begin
 
-text {*
+text \<open>
 the formulation of well-typedness of method calls given below (as well as
 the Java Specification 1.0) is a little too restrictive: Is does not allow
 methods of class Object to be called upon references of interface type.
@@ -19,7 +19,7 @@
   e.g.\ definedness of names (of parameters, locals, fields, methods)
 \end{itemize}
 \end{description}
-*}
+\<close>
 
 text "local variables, including method parameters and This:"
 type_synonym lenv = "vname \<rightharpoonup> ty"
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/JVM/JVMDefensive.thy
--- a/src/HOL/MicroJava/JVM/JVMDefensive.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/JVM/JVMDefensive.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -2,15 +2,15 @@
     Author:     Gerwin Klein
 *)
 
-section {* A Defensive JVM *}
+section \<open>A Defensive JVM\<close>
 
 theory JVMDefensive
 imports JVMExec
 begin
 
-text {*
+text \<open>
   Extend the state space by one element indicating a type error (or
-  other abnormal termination) *}
+  other abnormal termination)\<close>
 datatype 'a type_error = TypeError | Normal 'a
 
 
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/JVM/JVMExceptions.thy
--- a/src/HOL/MicroJava/JVM/JVMExceptions.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/JVM/JVMExceptions.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
     Copyright   2001 Technische Universitaet Muenchen
 *)
 
-section {* Exception handling in the JVM *}
+section \<open>Exception handling in the JVM\<close>
 
 theory JVMExceptions imports JVMInstructions begin
 
@@ -41,15 +41,15 @@
         | Some handler_pc \<Rightarrow> (None, hp, ([xc], loc, C, sig, handler_pc)#frs)))"
 
 
-text {*
+text \<open>
   System exceptions are allocated in all heaps:
-*}
+\<close>
 
 
-text {*
+text \<open>
   Only program counters that are mentioned in the exception table
   can be returned by @{term match_exception_table}:
-*}
+\<close>
 lemma match_exception_table_in_et:
   "match_exception_table G C pc et = Some pc' \<Longrightarrow> \<exists>e \<in> set et. pc' = fst (snd (snd e))"
   by (induct et) (auto split: split_if_asm)
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/JVM/JVMExec.thy
--- a/src/HOL/MicroJava/JVM/JVMExec.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/JVM/JVMExec.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -3,7 +3,7 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-section {* Program Execution in the JVM *}
+section \<open>Program Execution in the JVM\<close>
 
 theory JVMExec imports JVMExecInstr JVMExceptions begin
 
@@ -28,12 +28,12 @@
   "G \<turnstile> s \<midarrow>jvm\<rightarrow> t == (s,t) \<in> {(s,t). exec(G,s) = Some t}^*"
 
 
-text {*
+text \<open>
   The start configuration of the JVM: in the start heap, we call a 
   method @{text m} of class @{text C} in program @{text G}. The 
   @{text this} pointer of the frame is set to @{text Null} to simulate
   a static method invokation.
-*}
+\<close>
 definition start_state :: "jvm_prog \<Rightarrow> cname \<Rightarrow> mname \<Rightarrow> jvm_state" where
   "start_state G C m \<equiv>
   let (C',rT,mxs,mxl,i,et) = the (method (G,C) (m,[])) in
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/JVM/JVMExecInstr.thy
--- a/src/HOL/MicroJava/JVM/JVMExecInstr.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/JVM/JVMExecInstr.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -4,7 +4,7 @@
 *)
 
 
-section {* JVM Instruction Semantics *}
+section \<open>JVM Instruction Semantics\<close>
 
 
 theory JVMExecInstr imports JVMInstructions JVMState begin
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/JVM/JVMInstructions.thy
--- a/src/HOL/MicroJava/JVM/JVMInstructions.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/JVM/JVMInstructions.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -2,7 +2,7 @@
     Author:     Gerwin Klein, Technische Universitaet Muenchen
 *)
 
-section {* Instructions of the JVM *}
+section \<open>Instructions of the JVM\<close>
 
 
 theory JVMInstructions imports JVMState begin
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/JVM/JVMListExample.thy
--- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -2,16 +2,16 @@
     Author:     Stefan Berghofer
 *)
 
-section {* Example for generating executable code from JVM semantics \label{sec:JVMListExample} *}
+section \<open>Example for generating executable code from JVM semantics \label{sec:JVMListExample}\<close>
 
 theory JVMListExample
 imports "../J/SystemClasses" JVMExec
 begin
 
-text {*
+text \<open>
   Since the types @{typ cnam}, @{text vnam}, and @{text mname} are 
   anonymous, we describe distinctness of names in the example by axioms:
-*}
+\<close>
 axiomatization list_nam test_nam :: cnam
   where distinct_classes: "list_nam \<noteq> test_nam"
 
@@ -136,7 +136,7 @@
 definition
   "test = exec (E, start_state E test_name makelist_name)"
 
-ML_val {*
+ML_val \<open>
   @{code test}; 
   @{code exec} (@{code E}, @{code the} it);
   @{code exec} (@{code E}, @{code the} it);
@@ -191,6 +191,6 @@
   @{code exec} (@{code E}, @{code the} it);
   @{code exec} (@{code E}, @{code the} it);
   @{code exec} (@{code E}, @{code the} it);
-*}
+\<close>
 
 end
diff -r a273bdac0934 -r 8b5f00202e1a src/HOL/MicroJava/JVM/JVMState.thy
--- a/src/HOL/MicroJava/JVM/JVMState.thy	Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/JVM/JVMState.thy	Wed Oct 07 23:28:49 2015 +0200
@@ -2,15 +2,15 @@
     Author:     Cornelia Pusch, Gerwin Klein, Technische Universitaet Muenchen
 *)
 
-chapter {* Java Virtual Machine \label{cha:jvm} *}
+chapter \<open>Java Virtual Machine \label{cha:jvm}\<close>
 
-section {* State of the JVM *}
+section \<open>State of the JVM\<close>
 
 theory JVMState
 imports "../J/Conform"
 begin
 
-subsection {* Frame Stack *}
+subsection \<open>Frame Stack\<close>
 type_synonym opstack = "val list"
 type_synonym locvars = "val list"
 type_synonym p_count = nat
@@ -29,16 +29,16 @@
   -- "program counter within frame"
 
 
-subsection {* Exceptions *}
+subsection \<open>Exceptions\<close>
 definition raise_system_xcpt :: "bool \<Rightarrow> xcpt \<Rightarrow> val option" where
   "raise_system_xcpt b x \<equiv> raise_if b x None"
 
-subsection {* Runtime State *}
+subsection \<open>Runtime State\<close>
 type_synonym
   jvm_state = "val option \<times> aheap \<times> frame list"  -- "exception flag, heap, frames"
 
 
-subsection {* Lemmas *}
+subsection \<open>Lemmas\<close>
 
 lemma new_Addr_OutOfMemory:
   "snd (new_Addr hp) = Some xcp \<Longrightarrow> xcp = Addr (XcptRef OutOfMemory)"