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