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