1.1 --- a/src/FOL/ex/Nat2.thy	Tue May 03 11:28:51 1994 +0200
     1.2 +++ b/src/FOL/ex/Nat2.thy	Tue May 03 15:00:00 1994 +0200
     1.3 @@ -1,17 +1,18 @@
     1.4  (*  Title: 	FOL/ex/nat2.thy
     1.5      ID:         $Id$
     1.6      Author: 	Tobias Nipkow
     1.7 -    Copyright   1991  University of Cambridge
     1.8 +    Copyright   1994  University of Cambridge
     1.9  
    1.10  Theory for examples of simplification and induction on the natural numbers
    1.11  *)
    1.12  
    1.13  Nat2 = FOL +
    1.14  
    1.15 -types nat 0
    1.16 +types nat
    1.17  arities nat :: term
    1.18  
    1.19 -consts succ,pred :: "nat => nat"
    1.20 +consts
    1.21 + succ,pred :: "nat => nat"
    1.22         "0" :: "nat"	("0")
    1.23         "+" :: "[nat,nat] => nat" (infixr 90)
    1.24    "<","<=" :: "[nat,nat] => o"   (infixr 70)