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