# HG changeset patch
# User lcp
# Date 767970000 -7200
# Node ID fd3ab8bcb69dfed82ede8f12896dfcacb8294c4b
# Parent  1718ce07a584b2a9a43064955d3107857b15461a
removal of obsolete type-declaration syntax

diff -r 1718ce07a584 -r fd3ab8bcb69d src/FOL/ex/List.thy
--- a/src/FOL/ex/List.thy	Tue May 03 11:28:51 1994 +0200
+++ b/src/FOL/ex/List.thy	Tue May 03 15:00:00 1994 +0200
@@ -8,7 +8,7 @@
 
 List = Nat2 +
 
-types list 1
+types 'a list
 arities list :: (term)term
 
 consts
diff -r 1718ce07a584 -r fd3ab8bcb69d src/FOL/ex/Nat.thy
--- a/src/FOL/ex/Nat.thy	Tue May 03 11:28:51 1994 +0200
+++ b/src/FOL/ex/Nat.thy	Tue May 03 15:00:00 1994 +0200
@@ -11,12 +11,12 @@
 *)
 
 Nat = FOL +
-types   nat 0
-arities nat         :: term
-consts  "0"         :: "nat"    ("0")
-        Suc         :: "nat=>nat"
-        rec         :: "[nat, 'a, [nat,'a]=>'a] => 'a"
-        "+"         :: "[nat, nat] => nat"              (infixl 60)
+types   nat
+arities nat :: term
+consts  "0" :: "nat"    ("0")
+        Suc :: "nat=>nat"
+        rec :: "[nat, 'a, [nat,'a]=>'a] => 'a"
+        "+" :: "[nat, nat] => nat"              (infixl 60)
 rules   induct      "[| P(0);  !!x. P(x) ==> P(Suc(x)) |]  ==> P(n)"
         Suc_inject  "Suc(m)=Suc(n) ==> m=n"
         Suc_neq_0   "Suc(m)=0      ==> R"
diff -r 1718ce07a584 -r fd3ab8bcb69d src/FOL/ex/Nat2.thy
--- a/src/FOL/ex/Nat2.thy	Tue May 03 11:28:51 1994 +0200
+++ b/src/FOL/ex/Nat2.thy	Tue May 03 15:00:00 1994 +0200
@@ -1,17 +1,18 @@
 (*  Title: 	FOL/ex/nat2.thy
     ID:         $Id$
     Author: 	Tobias Nipkow
-    Copyright   1991  University of Cambridge
+    Copyright   1994  University of Cambridge
 
 Theory for examples of simplification and induction on the natural numbers
 *)
 
 Nat2 = FOL +
 
-types nat 0
+types nat
 arities nat :: term
 
-consts succ,pred :: "nat => nat"
+consts
+ succ,pred :: "nat => nat"
        "0" :: "nat"	("0")
        "+" :: "[nat,nat] => nat" (infixr 90)
   "<","<=" :: "[nat,nat] => o"   (infixr 70)
diff -r 1718ce07a584 -r fd3ab8bcb69d src/FOL/ex/Prolog.thy
--- a/src/FOL/ex/Prolog.thy	Tue May 03 11:28:51 1994 +0200
+++ b/src/FOL/ex/Prolog.thy	Tue May 03 15:00:00 1994 +0200
@@ -9,7 +9,7 @@
 *)
 
 Prolog = FOL +
-types   list 1
+types   'a list
 arities list    :: (term)term
 consts  Nil     :: "'a list"
         ":"     :: "['a, 'a list]=> 'a list"            (infixr 60)