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