--- a/Prod.thy Thu Aug 18 12:23:52 1994 +0200
+++ b/Prod.thy Thu Aug 18 12:38:12 1994 +0200
@@ -27,7 +27,7 @@
Abs_Prod :: "('a => 'b => bool) => 'a * 'b"
fst :: "'a * 'b => 'a"
snd :: "'a * 'b => 'b"
- split :: "['a * 'b, ['a,'b]=>'c] => 'c"
+ split :: "[['a,'b]=>'c, 'a * 'b] => 'c"
prod_fun :: "['a=>'b, 'c=>'d, 'a*'c] => 'b*'d"
Pair :: "['a,'b] => 'a * 'b"
"@Tuple" :: "args => 'a*'b" ("(1<_>)")
@@ -56,8 +56,8 @@
Pair_def "Pair(a,b) == Abs_Prod(Pair_Rep(a,b))"
fst_def "fst(p) == @a. ? b. p = <a,b>"
snd_def "snd(p) == @b. ? a. p = <a,b>"
- split_def "split(p,c) == c(fst(p),snd(p))"
- prod_fun_def "prod_fun(f,g) == (%z.split(z, %x y.<f(x), g(y)>))"
+ split_def "split(c,p) == c(fst(p),snd(p))"
+ prod_fun_def "prod_fun(f,g) == split(%x y.<f(x), g(y)>)"
Sigma_def "Sigma(A,B) == UN x:A. UN y:B(x). {<x,y>}"
Unit_def "Unit == {p. p=True}"