src/ZF/ZF.thy
changeset 14565 c6dc17aab88a
parent 14227 0356666744ec
child 14854 61bdf2ae4dc5
     1.1 --- a/src/ZF/ZF.thy	Wed Apr 14 13:28:46 2004 +0200
     1.2 +++ b/src/ZF/ZF.thy	Wed Apr 14 14:13:05 2004 +0200
     1.3 @@ -170,6 +170,25 @@
     1.4  
     1.5  syntax (HTML output)
     1.6    "op *"      :: "[i, i] => i"               (infixr "\<times>" 80)
     1.7 +  "op Int"    :: "[i, i] => i"    	     (infixl "\<inter>" 70)
     1.8 +  "op Un"     :: "[i, i] => i"    	     (infixl "\<union>" 65)
     1.9 +  "op <="     :: "[i, i] => o"    	     (infixl "\<subseteq>" 50)
    1.10 +  "op :"      :: "[i, i] => o"    	     (infixl "\<in>" 50)
    1.11 +  "op ~:"     :: "[i, i] => o"               (infixl "\<notin>" 50)
    1.12 +  "@Collect"  :: "[pttrn, i, o] => i"        ("(1{_ \<in> _ ./ _})")
    1.13 +  "@Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \<in> _, _})")
    1.14 +  "@RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _ \<in> _})" [51,0,51])
    1.15 +  "@UNION"    :: "[pttrn, i, i] => i"        ("(3\<Union>_\<in>_./ _)" 10)
    1.16 +  "@INTER"    :: "[pttrn, i, i] => i"        ("(3\<Inter>_\<in>_./ _)" 10)
    1.17 +  Union       :: "i =>i"                     ("\<Union>_" [90] 90)
    1.18 +  Inter       :: "i =>i"                     ("\<Inter>_" [90] 90)
    1.19 +  "@PROD"     :: "[pttrn, i, i] => i"        ("(3\<Pi>_\<in>_./ _)" 10)
    1.20 +  "@SUM"      :: "[pttrn, i, i] => i"        ("(3\<Sigma>_\<in>_./ _)" 10)
    1.21 +  "@lam"      :: "[pttrn, i, i] => i"        ("(3\<lambda>_\<in>_./ _)" 10)
    1.22 +  "@Ball"     :: "[pttrn, i, o] => o"        ("(3\<forall>_\<in>_./ _)" 10)
    1.23 +  "@Bex"      :: "[pttrn, i, o] => o"        ("(3\<exists>_\<in>_./ _)" 10)
    1.24 +  "@Tuple"    :: "[i, is] => i"              ("\<langle>(_,/ _)\<rangle>")
    1.25 +  "@pattern"  :: "patterns => pttrn"         ("\<langle>_\<rangle>")
    1.26  
    1.27  
    1.28  finalconsts