diff -r 4f6fd393713f -r cc421547e744 src/HOL/MicroJava/J/Example.thy
--- a/src/HOL/MicroJava/J/Example.thy	Mon Feb 05 14:59:44 2001 +0100
+++ b/src/HOL/MicroJava/J/Example.thy	Mon Feb 05 20:14:15 2001 +0100
@@ -2,14 +2,22 @@
     ID:         $Id$
     Author:     David von Oheimb
     Copyright   1997 Technische Universitaet Muenchen
+*)
 
-The following example Bali program includes:
+header "Example MicroJava Program"
+
+theory Example = Eval:
+
+text {* 
+The following example MicroJava program includes:
  class declarations with inheritance, hiding of fields, and overriding of
   methods (with refined result type), 
  instance creation, local assignment, sequential composition,
  method call with dynamic binding, literal values,
- expression statement, local access, type cast, field assignment (in part), skip
+ expression statement, local access, type cast, field assignment (in part), 
+ skip.
 
+\begin{verbatim}
 class Base {
   boolean vee;
   Base foo(Base x) {return x;}
@@ -26,9 +34,8 @@
     e.foo(null);
   }
 }
-*)
-
-theory Example = Eval:
+\end{verbatim}
+*}
 
 datatype cnam_ = Base_ | Ext_
 datatype vnam_ = vee_ | x_ | e_