# HG changeset patch
# User lcp
# Date 783623724 -3600
# Node ID 59a4fa76b5909494d11ae2d9dd2d225eafdd0e5c
# Parent  41b59e4c78c491a21e17a3903fb2c86de47a0e33
ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}

diff -r 41b59e4c78c4 -r 59a4fa76b590 src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Mon Oct 31 18:11:12 1994 +0100
+++ b/src/ZF/ZF.thy	Mon Oct 31 18:15:24 1994 +0100
@@ -16,91 +16,91 @@
 
 consts
 
-  "0"           :: "i"                  ("0")   (*the empty set*)
-  Pow           :: "i => i"                     (*power sets*)
-  Inf           :: "i"                          (*infinite set*)
+  "0"         :: "i"                  ("0")   (*the empty set*)
+  Pow         :: "i => i"                     (*power sets*)
+  Inf         :: "i"                          (*infinite set*)
 
   (* Bounded Quantifiers *)
 
-  Ball, Bex     :: "[i, i => o] => o"
+  Ball, Bex   :: "[i, i => o] => o"
 
   (* General Union and Intersection *)
 
-  Union, Inter  :: "i => i"
+  Union,Inter :: "i => i"
 
   (* Variations on Replacement *)
 
-  PrimReplace   :: "[i, [i, i] => o] => i"
-  Replace       :: "[i, [i, i] => o] => i"
-  RepFun        :: "[i, i => i] => i"
-  Collect       :: "[i, i => o] => i"
+  PrimReplace :: "[i, [i, i] => o] => i"
+  Replace     :: "[i, [i, i] => o] => i"
+  RepFun      :: "[i, i => i] => i"
+  Collect     :: "[i, i => o] => i"
 
   (* Descriptions *)
 
-  The           :: "(i => o) => i"      (binder "THE " 10)
-  if            :: "[o, i, i] => i"
+  The         :: "(i => o) => i"      (binder "THE " 10)
+  if          :: "[o, i, i] => i"
 
   (* Finite Sets *)
 
-  Upair, cons   :: "[i, i] => i"
-  succ          :: "i => i"
+  Upair, cons :: "[i, i] => i"
+  succ        :: "i => i"
 
   (* Ordered Pairing *)
 
-  Pair          :: "[i, i] => i"
-  fst, snd      :: "i => i"
-  split         :: "[[i, i] => i, i] => i"
-  fsplit        :: "[[i, i] => o, i] => o"
+  Pair        :: "[i, i] => i"
+  fst, snd    :: "i => i"
+  split       :: "[[i, i] => i, i] => i"
+  fsplit      :: "[[i, i] => o, i] => o"
 
   (* Sigma and Pi Operators *)
 
-  Sigma, Pi     :: "[i, i => i] => i"
+  Sigma, Pi   :: "[i, i => i] => i"
 
   (* Relations and Functions *)
 
-  domain        :: "i => i"
-  range         :: "i => i"
-  field         :: "i => i"
-  converse      :: "i => i"
-  Lambda        :: "[i, i => i] => i"
-  restrict      :: "[i, i] => i"
+  domain      :: "i => i"
+  range       :: "i => i"
+  field       :: "i => i"
+  converse    :: "i => i"
+  Lambda      :: "[i, i => i] => i"
+  restrict    :: "[i, i] => i"
 
   (* Infixes in order of decreasing precedence *)
 
-  "``"          :: "[i, i] => i"    (infixl 90) (*image*)
-  "-``"         :: "[i, i] => i"    (infixl 90) (*inverse image*)
-  "`"           :: "[i, i] => i"    (infixl 90) (*function application*)
-(*"*"           :: "[i, i] => i"    (infixr 80) (*Cartesian product*)*)
-  "Int"         :: "[i, i] => i"    (infixl 70) (*binary intersection*)
-  "Un"          :: "[i, i] => i"    (infixl 65) (*binary union*)
-  "-"           :: "[i, i] => i"    (infixl 65) (*set difference*)
-(*"->"          :: "[i, i] => i"    (infixr 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] => i"    (infixl 90) (*image*)
+  "-``"       :: "[i, i] => i"    (infixl 90) (*inverse image*)
+  "`"         :: "[i, i] => i"    (infixl 90) (*function application*)
+(*"*"         :: "[i, i] => i"    (infixr 80) (*Cartesian product*)*)
+  "Int"       :: "[i, i] => i"    (infixl 70) (*binary intersection*)
+  "Un"        :: "[i, i] => i"    (infixl 65) (*binary union*)
+  "-"         :: "[i, i] => i"    (infixl 65) (*set difference*)
+(*"->"        :: "[i, i] => i"    (infixr 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*)*)
 
 
 types
   is
 
 syntax
-  ""            :: "i => is"                    ("_")
-  "@Enum"       :: "[i, is] => is"              ("_,/ _")
-  "~:"          :: "[i, i] => o"                (infixl 50)
-  "@Finset"     :: "is => i"                    ("{(_)}")
-  "@Tuple"      :: "[i, is] => i"               ("<(_,/ _)>")
-  "@Collect"    :: "[idt, i, o] => i"           ("(1{_: _ ./ _})")
-  "@Replace"    :: "[idt, idt, i, o] => i"      ("(1{_ ./ _: _, _})")
-  "@RepFun"     :: "[i, idt, i] => i"           ("(1{_ ./ _: _})")
-  "@INTER"      :: "[idt, i, i] => i"           ("(3INT _:_./ _)" 10)
-  "@UNION"      :: "[idt, i, i] => i"           ("(3UN _:_./ _)" 10)
-  "@PROD"       :: "[idt, i, i] => i"           ("(3PROD _:_./ _)" 10)
-  "@SUM"        :: "[idt, i, i] => i"           ("(3SUM _:_./ _)" 10)
-  "->"          :: "[i, i] => i"                (infixr 60)
-  "*"           :: "[i, i] => i"                (infixr 80)
-  "@lam"        :: "[idt, i, i] => i"           ("(3lam _:_./ _)" 10)
-  "@Ball"       :: "[idt, i, o] => o"           ("(3ALL _:_./ _)" 10)
-  "@Bex"        :: "[idt, i, o] => o"           ("(3EX _:_./ _)" 10)
+  ""          :: "i => is"                 ("_")
+  "@Enum"     :: "[i, is] => is"           ("_,/ _")
+  "~:"        :: "[i, i] => o"             (infixl 50)
+  "@Finset"   :: "is => i"                 ("{(_)}")
+  "@Tuple"    :: "[i, is] => i"            ("<(_,/ _)>")
+  "@Collect"  :: "[idt, i, o] => i"        ("(1{_: _ ./ _})")
+  "@Replace"  :: "[idt, idt, i, o] => i"   ("(1{_ ./ _: _, _})")
+  "@RepFun"   :: "[i, idt, i] => i"        ("(1{_ ./ _: _})" [51,0,51])
+  "@INTER"    :: "[idt, i, i] => i"        ("(3INT _:_./ _)" 10)
+  "@UNION"    :: "[idt, i, i] => i"        ("(3UN _:_./ _)" 10)
+  "@PROD"     :: "[idt, i, i] => i"        ("(3PROD _:_./ _)" 10)
+  "@SUM"      :: "[idt, i, i] => i"        ("(3SUM _:_./ _)" 10)
+  "->"        :: "[i, i] => i"             (infixr 60)
+  "*"         :: "[i, i] => i"             (infixr 80)
+  "@lam"      :: "[idt, i, i] => i"        ("(3lam _:_./ _)" 10)
+  "@Ball"     :: "[idt, i, o] => o"        ("(3ALL _:_./ _)" 10)
+  "@Bex"      :: "[idt, i, o] => o"        ("(3EX _:_./ _)" 10)
 
 translations
   "x ~: y"      == "~ (x : y)"