src/HOL/MicroJava/J/SystemClasses.thy
changeset 62042 6c6ccf573479
parent 61361 8b5f00202e1a
--- a/src/HOL/MicroJava/J/SystemClasses.thy	Sat Jan 02 18:46:36 2016 +0100
+++ b/src/HOL/MicroJava/J/SystemClasses.thy	Sat Jan 02 18:48:45 2016 +0100
@@ -8,7 +8,7 @@
 theory SystemClasses imports Decl begin
 
 text \<open>
-  This theory provides definitions for the @{text Object} class,
+  This theory provides definitions for the \<open>Object\<close> class,
   and the system exceptions.
 \<close>