
diff -r 23a8c5ac35f8 -r 69916a850301 src/HOL/NanoJava/Example.thy
--- a/src/HOL/NanoJava/Example.thy	Sat Oct 17 01:05:59 2009 +0200
+++ b/src/HOL/NanoJava/Example.thy	Sat Oct 17 14:43:18 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/NanoJava/Example.thy
-    ID:         $Id$
     Author:     David von Oheimb
     Copyright   2001 Technische Universitaet Muenchen
 *)
@@ -30,9 +29,9 @@
 
   public static void main(String[] args) // test x+1=1+x
     {
-	Nat one = new Nat().suc();
-	Nat x   = new Nat().suc().suc().suc().suc();
-	Nat ok = x.suc().eq(x.add(one));
+        Nat one = new Nat().suc();
+        Nat x   = new Nat().suc().suc().suc().suc();
+        Nat ok = x.suc().eq(x.add(one));
         System.out.println(ok != null);
     }
 }




