--- 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
--- 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"
--- 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)
--- 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)