# HG changeset patch
# User wenzelm
# Date 750339300 -3600
# Node ID c78503b345c4f7f3309c41338baad5d5c67fdc47
# Parent  bc48a71464b02aa6ded0aca8aa4f70729747489b
"The" now a binder, removed translation;
improved encoding and translations of tuples;
added parse rules for -> and *, removed ndependent_tr;

diff -r bc48a71464b0 -r c78503b345c4 src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Mon Oct 11 12:30:38 1993 +0100
+++ b/src/ZF/ZF.thy	Mon Oct 11 12:35:00 1993 +0100
@@ -9,7 +9,7 @@
 ZF = FOL +
 
 types
-  i, is, syntax 0
+  i, is 0
 
 arities
   i :: term
@@ -46,8 +46,7 @@
 
   (* Descriptions *)
 
-  "@THE"       :: "[idt, o] => i"              ("(3THE _./ _)" 10)
-  The          :: "[i => o] => i"
+  The          :: "(i => o) => i"              (binder "THE " 10)
   if           :: "[o, i, i] => i"
 
   (* Enumerations of type i *)
@@ -64,7 +63,6 @@
   (* Ordered Pairing and n-Tuples *)
 
   "@Tuple"     :: "[i, is] => i"               ("<(_,/ _)>")
-  PAIR         :: "syntax"
   Pair         :: "[i, i] => i"
   fst, snd     :: "i => i"
   split        :: "[[i,i] => i, i] => i"
@@ -100,19 +98,14 @@
   " ->" :: "[i, i] => i"         ("(_ ->/ _)" [61, 60] 60) (*function space*)
   "<="  :: "[i, i] => o"         (infixl 50) (*subset relation*)
   ":"   :: "[i, i] => o"         (infixl 50) (*membership relation*)
-  "~:"   :: "[i, i] => o"        (infixl 50) (*negated membership relation*)
+  "~:"  :: "[i, i] => o"         (infixl 50) (*negated membership relation*)
 
 
 translations
   "{x, xs}"     == "cons(x, {xs})"
   "{x}"         == "cons(x, 0)"
-
-  "PAIR(x, Pair(y, z))" <= "Pair(x, Pair(y, z))"
-  "PAIR(x, PAIR(y, z))" <= "Pair(x, PAIR(y, z))"
-  "<x, y, z>"           <= "PAIR(x, <y, z>)"
-  "<x, y, z>"           == "Pair(x, <y, z>)"
-  "<x, y>"              == "Pair(x, y)"
-
+  "<x, y, z>"   == "<x, <y, z>>"
+  "<x, y>"      == "Pair(x, y)"
   "{x:A. P}"    == "Collect(A, %x. P)"
   "{y. x:A, Q}" == "Replace(A, %x y. Q)"
   "{f. x:A}"    == "RepFun(A, %x. f)"
@@ -120,11 +113,11 @@
   "UN x:A. B"   == "Union({B. x:A})"
   "PROD x:A. B" => "Pi(A, %x. B)"
   "SUM x:A. B"  => "Sigma(A, %x. B)"
-  "THE x. P"    == "The(%x. P)"
+  "A -> B"      => "Pi(A, _K(B))"
+  "A * B"       => "Sigma(A, _K(B))"
   "lam x:A. f"  == "Lambda(A, %x. f)"
   "ALL x:A. P"  == "Ball(A, %x. P)"
   "EX x:A. P"   == "Bex(A, %x. P)"
-
   "x ~: y"      == "~ (x:y)"
 
 
@@ -221,10 +214,7 @@
 
 (* 'Dependent' type operators *)
 
-val parse_translation =
-  [(" ->", ndependent_tr "Pi"),
-   (" *", ndependent_tr "Sigma")];
-
 val print_translation =
   [("Pi", dependent_tr' ("@PROD", " ->")),
    ("Sigma", dependent_tr' ("@SUM", " *"))];
+
diff -r bc48a71464b0 -r c78503b345c4 src/ZF/zf.thy
--- a/src/ZF/zf.thy	Mon Oct 11 12:30:38 1993 +0100
+++ b/src/ZF/zf.thy	Mon Oct 11 12:35:00 1993 +0100
@@ -9,7 +9,7 @@
 ZF = FOL +
 
 types
-  i, is, syntax 0
+  i, is 0
 
 arities
   i :: term
@@ -46,8 +46,7 @@
 
   (* Descriptions *)
 
-  "@THE"       :: "[idt, o] => i"              ("(3THE _./ _)" 10)
-  The          :: "[i => o] => i"
+  The          :: "(i => o) => i"              (binder "THE " 10)
   if           :: "[o, i, i] => i"
 
   (* Enumerations of type i *)
@@ -64,7 +63,6 @@
   (* Ordered Pairing and n-Tuples *)
 
   "@Tuple"     :: "[i, is] => i"               ("<(_,/ _)>")
-  PAIR         :: "syntax"
   Pair         :: "[i, i] => i"
   fst, snd     :: "i => i"
   split        :: "[[i,i] => i, i] => i"
@@ -100,19 +98,14 @@
   " ->" :: "[i, i] => i"         ("(_ ->/ _)" [61, 60] 60) (*function space*)
   "<="  :: "[i, i] => o"         (infixl 50) (*subset relation*)
   ":"   :: "[i, i] => o"         (infixl 50) (*membership relation*)
-  "~:"   :: "[i, i] => o"        (infixl 50) (*negated membership relation*)
+  "~:"  :: "[i, i] => o"         (infixl 50) (*negated membership relation*)
 
 
 translations
   "{x, xs}"     == "cons(x, {xs})"
   "{x}"         == "cons(x, 0)"
-
-  "PAIR(x, Pair(y, z))" <= "Pair(x, Pair(y, z))"
-  "PAIR(x, PAIR(y, z))" <= "Pair(x, PAIR(y, z))"
-  "<x, y, z>"           <= "PAIR(x, <y, z>)"
-  "<x, y, z>"           == "Pair(x, <y, z>)"
-  "<x, y>"              == "Pair(x, y)"
-
+  "<x, y, z>"   == "<x, <y, z>>"
+  "<x, y>"      == "Pair(x, y)"
   "{x:A. P}"    == "Collect(A, %x. P)"
   "{y. x:A, Q}" == "Replace(A, %x y. Q)"
   "{f. x:A}"    == "RepFun(A, %x. f)"
@@ -120,11 +113,11 @@
   "UN x:A. B"   == "Union({B. x:A})"
   "PROD x:A. B" => "Pi(A, %x. B)"
   "SUM x:A. B"  => "Sigma(A, %x. B)"
-  "THE x. P"    == "The(%x. P)"
+  "A -> B"      => "Pi(A, _K(B))"
+  "A * B"       => "Sigma(A, _K(B))"
   "lam x:A. f"  == "Lambda(A, %x. f)"
   "ALL x:A. P"  == "Ball(A, %x. P)"
   "EX x:A. P"   == "Bex(A, %x. P)"
-
   "x ~: y"      == "~ (x:y)"
 
 
@@ -221,10 +214,7 @@
 
 (* 'Dependent' type operators *)
 
-val parse_translation =
-  [(" ->", ndependent_tr "Pi"),
-   (" *", ndependent_tr "Sigma")];
-
 val print_translation =
   [("Pi", dependent_tr' ("@PROD", " ->")),
    ("Sigma", dependent_tr' ("@SUM", " *"))];
+