diff -r e653cb933293 -r 10e2d29a77de src/HOL/MicroJava/J/Example.thy
--- a/src/HOL/MicroJava/J/Example.thy	Tue Oct 17 08:00:46 2000 +0200
+++ b/src/HOL/MicroJava/J/Example.thy	Tue Oct 17 08:41:42 2000 +0200
@@ -15,7 +15,7 @@
   Base foo(Base x) {return x;}
 }
 
-class Ext extends Base{
+class Ext extends Base {
   int vee;
   Ext foo(Base x) {((Ext)x).vee=1; return null;}
 }