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