--- 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,[],[]))"