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;