src/HOL/NanoJava/Example.thy

 (*  Title:      HOL/NanoJava/Example.thy
-    ID:         $Id$
     Author:     David von Oheimb
     Copyright   2001 Technische Universitaet Muenchen
 *)
 
 header "Example"

   Nat add(Nat n)
     { if (this.pred != null) return this.pred.add(n.suc()); else return n; }
 
   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);
     }
 }
 \end{verbatim}