--- a/LList.thy Thu Mar 17 14:08:08 1994 +0100
+++ b/LList.thy Thu Mar 17 17:02:49 1994 +0100
@@ -24,8 +24,13 @@
*)
LList = Gfp + List +
-types llist 1
-arities llist :: (term)term
+
+types
+ 'a llist
+
+arities
+ llist :: (term)term
+
consts
LList :: "'a node set set => 'a node set set"
LListD_Fun ::
--- a/Nat.thy Thu Mar 17 14:08:08 1994 +0100
+++ b/Nat.thy Thu Mar 17 17:02:49 1994 +0100
@@ -9,9 +9,14 @@
*)
Nat = WF +
-types ind,nat 0
-arities ind,nat :: term
- nat :: ord
+
+types
+ ind
+ nat
+
+arities
+ ind,nat :: term
+ nat :: ord
consts
Zero_Rep :: "ind"
--- a/Prod.thy Thu Mar 17 14:08:08 1994 +0100
+++ b/Prod.thy Thu Mar 17 17:02:49 1994 +0100
@@ -11,29 +11,32 @@
*)
Prod = Set +
+
types
- "*" 2 (infixr 20)
- unit
+ ('a,'b) "*" (infixr 20)
+ unit
+
arities
- "*" :: (term,term)term
- unit :: term
+ "*" :: (term,term)term
+ unit :: term
+
consts
- Pair_Rep :: "['a,'b] => ['a,'b] => bool"
- Prod :: "('a => 'b => bool)set"
- Rep_Prod :: "'a * 'b => ('a => 'b => bool)"
- Abs_Prod :: "('a => 'b => bool) => 'a * 'b"
- fst :: "'a * 'b => 'a"
- snd :: "'a * 'b => 'b"
- split :: "['a * 'b, ['a,'b]=>'c] => 'c"
- prod_fun :: "['a=>'b, 'c=>'d, 'a*'c] => 'b*'d"
- Pair :: "['a,'b] => 'a * 'b"
- "@Tuple" :: "args => 'a*'b" ("(1<_>)")
- Sigma :: "['a set, 'a => 'b set] => ('a*'b)set"
+ Pair_Rep :: "['a,'b] => ['a,'b] => bool"
+ Prod :: "('a => 'b => bool)set"
+ Rep_Prod :: "'a * 'b => ('a => 'b => bool)"
+ Abs_Prod :: "('a => 'b => bool) => 'a * 'b"
+ fst :: "'a * 'b => 'a"
+ snd :: "'a * 'b => 'b"
+ split :: "['a * 'b, ['a,'b]=>'c] => 'c"
+ prod_fun :: "['a=>'b, 'c=>'d, 'a*'c] => 'b*'d"
+ Pair :: "['a,'b] => 'a * 'b"
+ "@Tuple" :: "args => 'a*'b" ("(1<_>)")
+ Sigma :: "['a set, 'a => 'b set] => ('a*'b)set"
- Unit :: "bool set"
- Rep_Unit :: "unit => bool"
- Abs_Unit :: "bool => unit"
- Unity :: "unit" ("<>")
+ Unit :: "bool set"
+ Rep_Unit :: "unit => bool"
+ Abs_Unit :: "bool => unit"
+ Unity :: "unit" ("<>")
translations
--- a/Sum.thy Thu Mar 17 14:08:08 1994 +0100
+++ b/Sum.thy Thu Mar 17 17:02:49 1994 +0100
@@ -7,17 +7,23 @@
*)
Sum = Prod +
-types "+" 2 (infixl 10)
-arities "+" :: (term,term)term
+
+types
+ ('a,'b) "+" (infixl 10)
+
+arities
+ "+" :: (term,term)term
+
consts
- Inl_Rep :: "['a,'a,'b,bool] => bool"
- Inr_Rep :: "['b,'a,'b,bool] => bool"
- Sum :: "(['a,'b,bool] => bool)set"
- Rep_Sum :: "'a + 'b => (['a,'b,bool] => bool)"
- Abs_Sum :: "(['a,'b,bool] => bool) => 'a+'b"
- Inl :: "'a => 'a+'b"
- Inr :: "'b => 'a+'b"
- sum_case :: "['a+'b, 'a=>'c,'b=>'c] =>'c"
+ Inl_Rep :: "['a,'a,'b,bool] => bool"
+ Inr_Rep :: "['b,'a,'b,bool] => bool"
+ Sum :: "(['a,'b,bool] => bool)set"
+ Rep_Sum :: "'a + 'b => (['a,'b,bool] => bool)"
+ Abs_Sum :: "(['a,'b,bool] => bool) => 'a+'b"
+ Inl :: "'a => 'a+'b"
+ Inr :: "'b => 'a+'b"
+ sum_case :: "['a+'b, 'a=>'c,'b=>'c] =>'c"
+
rules
Inl_Rep_def "Inl_Rep == (%a. %x y p. x=a & p)"
Inr_Rep_def "Inr_Rep == (%b. %x y p. y=b & ~p)"
--- a/Univ.thy Thu Mar 17 14:08:08 1994 +0100
+++ b/Univ.thy Thu Mar 17 17:02:49 1994 +0100
@@ -12,8 +12,13 @@
*)
Univ = Arith +
-types node 1
-arities node :: (term)term
+
+types
+ 'a node
+
+arities
+ node :: (term)term
+
consts
Least :: "(nat=>bool) => nat" (binder "LEAST " 10)
--- a/llist.thy Thu Mar 17 14:08:08 1994 +0100
+++ b/llist.thy Thu Mar 17 17:02:49 1994 +0100
@@ -24,8 +24,13 @@
*)
LList = Gfp + List +
-types llist 1
-arities llist :: (term)term
+
+types
+ 'a llist
+
+arities
+ llist :: (term)term
+
consts
LList :: "'a node set set => 'a node set set"
LListD_Fun ::
--- a/nat.thy Thu Mar 17 14:08:08 1994 +0100
+++ b/nat.thy Thu Mar 17 17:02:49 1994 +0100
@@ -9,9 +9,14 @@
*)
Nat = WF +
-types ind,nat 0
-arities ind,nat :: term
- nat :: ord
+
+types
+ ind
+ nat
+
+arities
+ ind,nat :: term
+ nat :: ord
consts
Zero_Rep :: "ind"
--- a/prod.thy Thu Mar 17 14:08:08 1994 +0100
+++ b/prod.thy Thu Mar 17 17:02:49 1994 +0100
@@ -11,29 +11,32 @@
*)
Prod = Set +
+
types
- "*" 2 (infixr 20)
- unit
+ ('a,'b) "*" (infixr 20)
+ unit
+
arities
- "*" :: (term,term)term
- unit :: term
+ "*" :: (term,term)term
+ unit :: term
+
consts
- Pair_Rep :: "['a,'b] => ['a,'b] => bool"
- Prod :: "('a => 'b => bool)set"
- Rep_Prod :: "'a * 'b => ('a => 'b => bool)"
- Abs_Prod :: "('a => 'b => bool) => 'a * 'b"
- fst :: "'a * 'b => 'a"
- snd :: "'a * 'b => 'b"
- split :: "['a * 'b, ['a,'b]=>'c] => 'c"
- prod_fun :: "['a=>'b, 'c=>'d, 'a*'c] => 'b*'d"
- Pair :: "['a,'b] => 'a * 'b"
- "@Tuple" :: "args => 'a*'b" ("(1<_>)")
- Sigma :: "['a set, 'a => 'b set] => ('a*'b)set"
+ Pair_Rep :: "['a,'b] => ['a,'b] => bool"
+ Prod :: "('a => 'b => bool)set"
+ Rep_Prod :: "'a * 'b => ('a => 'b => bool)"
+ Abs_Prod :: "('a => 'b => bool) => 'a * 'b"
+ fst :: "'a * 'b => 'a"
+ snd :: "'a * 'b => 'b"
+ split :: "['a * 'b, ['a,'b]=>'c] => 'c"
+ prod_fun :: "['a=>'b, 'c=>'d, 'a*'c] => 'b*'d"
+ Pair :: "['a,'b] => 'a * 'b"
+ "@Tuple" :: "args => 'a*'b" ("(1<_>)")
+ Sigma :: "['a set, 'a => 'b set] => ('a*'b)set"
- Unit :: "bool set"
- Rep_Unit :: "unit => bool"
- Abs_Unit :: "bool => unit"
- Unity :: "unit" ("<>")
+ Unit :: "bool set"
+ Rep_Unit :: "unit => bool"
+ Abs_Unit :: "bool => unit"
+ Unity :: "unit" ("<>")
translations
--- a/sum.thy Thu Mar 17 14:08:08 1994 +0100
+++ b/sum.thy Thu Mar 17 17:02:49 1994 +0100
@@ -7,17 +7,23 @@
*)
Sum = Prod +
-types "+" 2 (infixl 10)
-arities "+" :: (term,term)term
+
+types
+ ('a,'b) "+" (infixl 10)
+
+arities
+ "+" :: (term,term)term
+
consts
- Inl_Rep :: "['a,'a,'b,bool] => bool"
- Inr_Rep :: "['b,'a,'b,bool] => bool"
- Sum :: "(['a,'b,bool] => bool)set"
- Rep_Sum :: "'a + 'b => (['a,'b,bool] => bool)"
- Abs_Sum :: "(['a,'b,bool] => bool) => 'a+'b"
- Inl :: "'a => 'a+'b"
- Inr :: "'b => 'a+'b"
- sum_case :: "['a+'b, 'a=>'c,'b=>'c] =>'c"
+ Inl_Rep :: "['a,'a,'b,bool] => bool"
+ Inr_Rep :: "['b,'a,'b,bool] => bool"
+ Sum :: "(['a,'b,bool] => bool)set"
+ Rep_Sum :: "'a + 'b => (['a,'b,bool] => bool)"
+ Abs_Sum :: "(['a,'b,bool] => bool) => 'a+'b"
+ Inl :: "'a => 'a+'b"
+ Inr :: "'b => 'a+'b"
+ sum_case :: "['a+'b, 'a=>'c,'b=>'c] =>'c"
+
rules
Inl_Rep_def "Inl_Rep == (%a. %x y p. x=a & p)"
Inr_Rep_def "Inr_Rep == (%b. %x y p. y=b & ~p)"
--- a/univ.thy Thu Mar 17 14:08:08 1994 +0100
+++ b/univ.thy Thu Mar 17 17:02:49 1994 +0100
@@ -12,8 +12,13 @@
*)
Univ = Arith +
-types node 1
-arities node :: (term)term
+
+types
+ 'a node
+
+arities
+ node :: (term)term
+
consts
Least :: "(nat=>bool) => nat" (binder "LEAST " 10)