# HG changeset patch
# User wenzelm
# Date 1451493537 -3600
# Node ID d68b705719ce657f25f5d1188139e34b59867fbe
# Parent  7ab2dc7ba8f8d5a76fa1468a87142187c2664531
clarified print modes;

diff -r 7ab2dc7ba8f8 -r d68b705719ce src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Wed Dec 30 17:18:32 2015 +0100
+++ b/src/ZF/ZF.thy	Wed Dec 30 17:38:57 2015 +0100
@@ -25,8 +25,8 @@
   Bex   :: "[i, i => o] => o"
 
 text \<open>General Union and Intersection\<close>
-axiomatization Union :: "i => i"
-consts Inter :: "i => i"
+axiomatization Union :: "i => i"  ("\<Union>_" [90] 90)
+consts Inter :: "i => i"  ("\<Inter>_" [90] 90)
 
 text \<open>Variations on Replacement\<close>
 axiomatization PrimReplace :: "[i, [i, i] => o] => i"
@@ -76,29 +76,28 @@
 
 text \<open>Infixes in order of decreasing precedence\<close>
 consts
-
   Image       :: "[i, i] => i"    (infixl "``" 90) \<comment>\<open>image\<close>
   vimage      :: "[i, i] => i"    (infixl "-``" 90) \<comment>\<open>inverse image\<close>
   "apply"     :: "[i, i] => i"    (infixl "`" 90) \<comment>\<open>function application\<close>
-  "Int"       :: "[i, i] => i"    (infixl "Int" 70) \<comment>\<open>binary intersection\<close>
-  "Un"        :: "[i, i] => i"    (infixl "Un" 65) \<comment>\<open>binary union\<close>
+  "Int"       :: "[i, i] => i"    (infixl "\<inter>" 70) \<comment>\<open>binary intersection\<close>
+  "Un"        :: "[i, i] => i"    (infixl "\<union>" 65) \<comment>\<open>binary union\<close>
   Diff        :: "[i, i] => i"    (infixl "-" 65) \<comment>\<open>set difference\<close>
-  Subset      :: "[i, i] => o"    (infixl "<=" 50) \<comment>\<open>subset relation\<close>
+  Subset      :: "[i, i] => o"    (infixl "\<subseteq>" 50) \<comment>\<open>subset relation\<close>
 
 axiomatization
-  mem         :: "[i, i] => o"    (infixl ":" 50) \<comment>\<open>membership relation\<close>
+  mem         :: "[i, i] => o"    (infixl "\<in>" 50) \<comment>\<open>membership relation\<close>
 
 abbreviation
-  not_mem :: "[i, i] => o"  (infixl "~:" 50)  \<comment>\<open>negated membership relation\<close>
-  where "x ~: y == ~ (x : y)"
+  not_mem :: "[i, i] => o"  (infixl "\<notin>" 50)  \<comment>\<open>negated membership relation\<close>
+  where "x \<notin> y \<equiv> \<not> (x \<in> y)"
 
 abbreviation
-  cart_prod :: "[i, i] => i"    (infixr "*" 80) \<comment>\<open>Cartesian product\<close>
-  where "A * B == Sigma(A, %_. B)"
+  cart_prod :: "[i, i] => i"    (infixr "\<times>" 80) \<comment>\<open>Cartesian product\<close>
+  where "A \<times> B \<equiv> Sigma(A, \<lambda>_. B)"
 
 abbreviation
   function_space :: "[i, i] => i"  (infixr "->" 60) \<comment>\<open>function space\<close>
-  where "A -> B == Pi(A, %_. B)"
+  where "A -> B \<equiv> Pi(A, \<lambda>_. B)"
 
 
 nonterminal "is" and patterns
@@ -108,68 +107,66 @@
   "_Enum"     :: "[i, is] => is"             ("_,/ _")
 
   "_Finset"   :: "is => i"                   ("{(_)}")
-  "_Tuple"    :: "[i, is] => i"              ("<(_,/ _)>")
-  "_Collect"  :: "[pttrn, i, o] => i"        ("(1{_: _ ./ _})")
-  "_Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _: _, _})")
-  "_RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _: _})" [51,0,51])
-  "_INTER"    :: "[pttrn, i, i] => i"        ("(3INT _:_./ _)" 10)
-  "_UNION"    :: "[pttrn, i, i] => i"        ("(3UN _:_./ _)" 10)
-  "_PROD"     :: "[pttrn, i, i] => i"        ("(3PROD _:_./ _)" 10)
-  "_SUM"      :: "[pttrn, i, i] => i"        ("(3SUM _:_./ _)" 10)
-  "_lam"      :: "[pttrn, i, i] => i"        ("(3lam _:_./ _)" 10)
-  "_Ball"     :: "[pttrn, i, o] => o"        ("(3ALL _:_./ _)" 10)
-  "_Bex"      :: "[pttrn, i, o] => o"        ("(3EX _:_./ _)" 10)
+  "_Tuple"    :: "[i, is] => i"              ("\<langle>(_,/ _)\<rangle>")
+  "_Collect"  :: "[pttrn, i, o] => i"        ("(1{_ \<in> _ ./ _})")
+  "_Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \<in> _, _})")
+  "_RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _ \<in> _})" [51,0,51])
+  "_UNION"    :: "[pttrn, i, i] => i"        ("(3\<Union>_\<in>_./ _)" 10)
+  "_INTER"    :: "[pttrn, i, i] => i"        ("(3\<Inter>_\<in>_./ _)" 10)
+  "_PROD"     :: "[pttrn, i, i] => i"        ("(3\<Pi> _\<in>_./ _)" 10)
+  "_SUM"      :: "[pttrn, i, i] => i"        ("(3\<Sigma> _\<in>_./ _)" 10)
+  "_lam"      :: "[pttrn, i, i] => i"        ("(3\<lambda>_\<in>_./ _)" 10)
+  "_Ball"     :: "[pttrn, i, o] => o"        ("(3\<forall>_\<in>_./ _)" 10)
+  "_Bex"      :: "[pttrn, i, o] => o"        ("(3\<exists>_\<in>_./ _)" 10)
 
   (** Patterns -- extends pre-defined type "pttrn" used in abstractions **)
 
-  "_pattern"  :: "patterns => pttrn"         ("<_>")
+  "_pattern"  :: "patterns => pttrn"         ("\<langle>_\<rangle>")
   ""          :: "pttrn => patterns"         ("_")
   "_patterns" :: "[pttrn, patterns] => patterns"  ("_,/_")
 
 translations
   "{x, xs}"     == "CONST cons(x, {xs})"
   "{x}"         == "CONST cons(x, 0)"
-  "{x:A. P}"    == "CONST Collect(A, %x. P)"
-  "{y. x:A, Q}" == "CONST Replace(A, %x y. Q)"
-  "{b. x:A}"    == "CONST RepFun(A, %x. b)"
-  "INT x:A. B"  == "CONST Inter({B. x:A})"
-  "UN x:A. B"   == "CONST Union({B. x:A})"
-  "PROD x:A. B" == "CONST Pi(A, %x. B)"
-  "SUM x:A. B"  == "CONST Sigma(A, %x. B)"
-  "lam x:A. f"  == "CONST Lambda(A, %x. f)"
-  "ALL x:A. P"  == "CONST Ball(A, %x. P)"
-  "EX x:A. P"   == "CONST Bex(A, %x. P)"
+  "{x\<in>A. P}"    == "CONST Collect(A, \<lambda>x. P)"
+  "{y. x\<in>A, Q}" == "CONST Replace(A, \<lambda>x y. Q)"
+  "{b. x\<in>A}"    == "CONST RepFun(A, \<lambda>x. b)"
+  "\<Inter>x\<in>A. B"    == "CONST Inter({B. x\<in>A})"
+  "\<Union>x\<in>A. B"    == "CONST Union({B. x\<in>A})"
+  "\<Pi> x\<in>A. B"   == "CONST Pi(A, \<lambda>x. B)"
+  "\<Sigma> x\<in>A. B"   == "CONST Sigma(A, \<lambda>x. B)"
+  "\<lambda>x\<in>A. f"    == "CONST Lambda(A, \<lambda>x. f)"
+  "\<forall>x\<in>A. P"    == "CONST Ball(A, \<lambda>x. P)"
+  "\<exists>x\<in>A. P"    == "CONST Bex(A, \<lambda>x. P)"
 
-  "<x, y, z>"   == "<x, <y, z>>"
-  "<x, y>"      == "CONST Pair(x, y)"
-  "%<x,y,zs>.b" == "CONST split(%x <y,zs>.b)"
-  "%<x,y>.b"    == "CONST split(%x y. b)"
+  "\<langle>x, y, z\<rangle>"   == "\<langle>x, \<langle>y, z\<rangle>\<rangle>"
+  "\<langle>x, y\<rangle>"      == "CONST Pair(x, y)"
+  "\<lambda>\<langle>x,y,zs\<rangle>.b" == "CONST split(\<lambda>x \<langle>y,zs\<rangle>.b)"
+  "\<lambda>\<langle>x,y\<rangle>.b"    == "CONST split(\<lambda>x y. b)"
 
 
-notation (xsymbols)
-  cart_prod       (infixr "\<times>" 80) and
-  Int             (infixl "\<inter>" 70) and
-  Un              (infixl "\<union>" 65) and
+notation (ASCII)
+  cart_prod       (infixr "*" 80) and
+  Int             (infixl "Int" 70) and
+  Un              (infixl "Un" 65) and
   function_space  (infixr "\<rightarrow>" 60) and
-  Subset          (infixl "\<subseteq>" 50) and
-  mem             (infixl "\<in>" 50) and
-  not_mem         (infixl "\<notin>" 50) and
-  Union           ("\<Union>_" [90] 90) and
-  Inter           ("\<Inter>_" [90] 90)
+  Subset          (infixl "<=" 50) and
+  mem             (infixl ":" 50) and
+  not_mem         (infixl "~:" 50)
 
-syntax (xsymbols)
-  "_Collect"  :: "[pttrn, i, o] => i"        ("(1{_ \<in> _ ./ _})")
-  "_Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \<in> _, _})")
-  "_RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _ \<in> _})" [51,0,51])
-  "_UNION"    :: "[pttrn, i, i] => i"        ("(3\<Union>_\<in>_./ _)" 10)
-  "_INTER"    :: "[pttrn, i, i] => i"        ("(3\<Inter>_\<in>_./ _)" 10)
-  "_PROD"     :: "[pttrn, i, i] => i"        ("(3\<Pi>_\<in>_./ _)" 10)
-  "_SUM"      :: "[pttrn, i, i] => i"        ("(3\<Sigma>_\<in>_./ _)" 10)
-  "_lam"      :: "[pttrn, i, i] => i"        ("(3\<lambda>_\<in>_./ _)" 10)
-  "_Ball"     :: "[pttrn, i, o] => o"        ("(3\<forall>_\<in>_./ _)" 10)
-  "_Bex"      :: "[pttrn, i, o] => o"        ("(3\<exists>_\<in>_./ _)" 10)
-  "_Tuple"    :: "[i, is] => i"              ("\<langle>(_,/ _)\<rangle>")
-  "_pattern"  :: "patterns => pttrn"         ("\<langle>_\<rangle>")
+syntax (ASCII)
+  "_Collect"  :: "[pttrn, i, o] => i"        ("(1{_: _ ./ _})")
+  "_Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _: _, _})")
+  "_RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _: _})" [51,0,51])
+  "_UNION"    :: "[pttrn, i, i] => i"        ("(3UN _:_./ _)" 10)
+  "_INTER"    :: "[pttrn, i, i] => i"        ("(3INT _:_./ _)" 10)
+  "_PROD"     :: "[pttrn, i, i] => i"        ("(3PROD _:_./ _)" 10)
+  "_SUM"      :: "[pttrn, i, i] => i"        ("(3SUM _:_./ _)" 10)
+  "_lam"      :: "[pttrn, i, i] => i"        ("(3lam _:_./ _)" 10)
+  "_Ball"     :: "[pttrn, i, o] => o"        ("(3ALL _:_./ _)" 10)
+  "_Bex"      :: "[pttrn, i, o] => o"        ("(3EX _:_./ _)" 10)
+  "_Tuple"    :: "[i, is] => i"              ("<(_,/ _)>")
+  "_pattern"  :: "patterns => pttrn"         ("<_>")
 
 defs  (* Bounded Quantifiers *)
   Ball_def:      "Ball(A, P) == \<forall>x. x\<in>A \<longrightarrow> P(x)"
@@ -629,4 +626,3 @@
 by (best elim!: equalityCE del: ReplaceI RepFun_eqI)
 
 end
-