--- 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;}
}