src/ZF/ZF.thy
changeset 9965 1971c8dd0971
parent 9683 f87c8c449018
child 11233 34c81a796ee3
equal deleted inserted replaced
9964:7966a2902266 9965:1971c8dd0971
   151   "op :"      :: [i, i] => o    	   (infixl "\\<in>" 50)
   151   "op :"      :: [i, i] => o    	   (infixl "\\<in>" 50)
   152   "op ~:"     :: [i, i] => o               (infixl "\\<notin>" 50)
   152   "op ~:"     :: [i, i] => o               (infixl "\\<notin>" 50)
   153   "@Collect"  :: [pttrn, i, o] => i        ("(1{_\\<in> _ ./ _})")
   153   "@Collect"  :: [pttrn, i, o] => i        ("(1{_\\<in> _ ./ _})")
   154   "@Replace"  :: [pttrn, pttrn, i, o] => i ("(1{_ ./ _\\<in> _, _})")
   154   "@Replace"  :: [pttrn, pttrn, i, o] => i ("(1{_ ./ _\\<in> _, _})")
   155   "@RepFun"   :: [i, pttrn, i] => i        ("(1{_ ./ _\\<in> _})" [51,0,51])
   155   "@RepFun"   :: [i, pttrn, i] => i        ("(1{_ ./ _\\<in> _})" [51,0,51])
   156   "@INTER"    :: [pttrn, i, i] => i        ("(3\\<Inter> _\\<in>_./ _)" 10)
   156   "@INTER"    :: [pttrn, i, i] => i        ("(3\\<Inter>_\\<in>_./ _)" 10)
   157   "@UNION"    :: [pttrn, i, i] => i        ("(3\\<Union> _\\<in>_./ _)" 10)
   157   "@UNION"    :: [pttrn, i, i] => i        ("(3\\<Union>_\\<in>_./ _)" 10)
   158   "@PROD"     :: [pttrn, i, i] => i        ("(3\\<Pi> _\\<in>_./ _)" 10)
   158   "@PROD"     :: [pttrn, i, i] => i        ("(3\\<Pi>_\\<in>_./ _)" 10)
   159   "@SUM"      :: [pttrn, i, i] => i        ("(3\\<Sigma> _\\<in>_./ _)" 10)
   159   "@SUM"      :: [pttrn, i, i] => i        ("(3\\<Sigma>_\\<in>_./ _)" 10)
   160   "@lam"      :: [pttrn, i, i] => i        ("(3\\<lambda> _:_./ _)" 10)
   160   "@lam"      :: [pttrn, i, i] => i        ("(3\\<lambda>_:_./ _)" 10)
   161   "@Ball"     :: [pttrn, i, o] => o        ("(3\\<forall> _\\<in>_./ _)" 10)
   161   "@Ball"     :: [pttrn, i, o] => o        ("(3\\<forall>_\\<in>_./ _)" 10)
   162   "@Bex"      :: [pttrn, i, o] => o        ("(3\\<exists> _\\<in>_./ _)" 10)
   162   "@Bex"      :: [pttrn, i, o] => o        ("(3\\<exists>_\\<in>_./ _)" 10)
   163 (*
   163 
       
   164 syntax (xsymbols)
   164   "@Tuple"    :: [i, is] => i              ("\\<langle>(_,/ _)\\<rangle>")
   165   "@Tuple"    :: [i, is] => i              ("\\<langle>(_,/ _)\\<rangle>")
   165   "@pattern"  :: patterns => pttrn         ("\\<langle>_\\<rangle>")
   166   "@pattern"  :: patterns => pttrn         ("\\<langle>_\\<rangle>")
   166 *)
       
   167 
   167 
   168 syntax (HTML output)
   168 syntax (HTML output)
   169   "op *"      :: [i, i] => i               (infixr "\\<times>" 80)
   169   "op *"      :: [i, i] => i               (infixr "\\<times>" 80)
   170 
   170 
   171 
   171