1.1 --- a/src/FOL/ex/List.thy	Tue May 03 11:28:51 1994 +0200
     1.2 +++ b/src/FOL/ex/List.thy	Tue May 03 15:00:00 1994 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  
     1.5  List = Nat2 +
     1.6  
     1.7 -types list 1
     1.8 +types 'a list
     1.9  arities list :: (term)term
    1.10  
    1.11  consts

     2.1 --- a/src/FOL/ex/Nat.thy	Tue May 03 11:28:51 1994 +0200
     2.2 +++ b/src/FOL/ex/Nat.thy	Tue May 03 15:00:00 1994 +0200
     2.3 @@ -11,12 +11,12 @@
     2.4  *)
     2.5  
     2.6  Nat = FOL +
     2.7 -types   nat 0
     2.8 -arities nat         :: term
     2.9 -consts  "0"         :: "nat"    ("0")
    2.10 -        Suc         :: "nat=>nat"
    2.11 -        rec         :: "[nat, 'a, [nat,'a]=>'a] => 'a"
    2.12 -        "+"         :: "[nat, nat] => nat"              (infixl 60)
    2.13 +types   nat
    2.14 +arities nat :: term
    2.15 +consts  "0" :: "nat"    ("0")
    2.16 +        Suc :: "nat=>nat"
    2.17 +        rec :: "[nat, 'a, [nat,'a]=>'a] => 'a"
    2.18 +        "+" :: "[nat, nat] => nat"              (infixl 60)
    2.19  rules   induct      "[| P(0);  !!x. P(x) ==> P(Suc(x)) |]  ==> P(n)"
    2.20          Suc_inject  "Suc(m)=Suc(n) ==> m=n"
    2.21          Suc_neq_0   "Suc(m)=0      ==> R"

     3.1 --- a/src/FOL/ex/Nat2.thy	Tue May 03 11:28:51 1994 +0200
     3.2 +++ b/src/FOL/ex/Nat2.thy	Tue May 03 15:00:00 1994 +0200
     3.3 @@ -1,17 +1,18 @@
     3.4  (*  Title: 	FOL/ex/nat2.thy
     3.5      ID:         $Id$
     3.6      Author: 	Tobias Nipkow
     3.7 -    Copyright   1991  University of Cambridge
     3.8 +    Copyright   1994  University of Cambridge
     3.9  
    3.10  Theory for examples of simplification and induction on the natural numbers
    3.11  *)
    3.12  
    3.13  Nat2 = FOL +
    3.14  
    3.15 -types nat 0
    3.16 +types nat
    3.17  arities nat :: term
    3.18  
    3.19 -consts succ,pred :: "nat => nat"
    3.20 +consts
    3.21 + succ,pred :: "nat => nat"
    3.22         "0" :: "nat"	("0")
    3.23         "+" :: "[nat,nat] => nat" (infixr 90)
    3.24    "<","<=" :: "[nat,nat] => o"   (infixr 70)

     4.1 --- a/src/FOL/ex/Prolog.thy	Tue May 03 11:28:51 1994 +0200
     4.2 +++ b/src/FOL/ex/Prolog.thy	Tue May 03 15:00:00 1994 +0200
     4.3 @@ -9,7 +9,7 @@
     4.4  *)
     4.5  
     4.6  Prolog = FOL +
     4.7 -types   list 1
     4.8 +types   'a list
     4.9  arities list    :: (term)term
    4.10  consts  Nil     :: "'a list"
    4.11          ":"     :: "['a, 'a list]=> 'a list"            (infixr 60)