Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/ZF/ZF.thy
changeset 12552 d2d2ab3f1f37
parent 12114 a8e860c86252
child 12762 a0c0a1e3a53a 
--- a/src/ZF/ZF.thy	Wed Dec 19 11:07:38 2001 +0100
+++ b/src/ZF/ZF.thy	Wed Dec 19 11:13:27 2001 +0100
@@ -153,8 +153,10 @@
   "@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)
-  "@UNION"    :: [pttrn, i, i] => i        ("(3\\<Union>_\\<in>_./ _)" 10)
+  Union       :: i =>i                     ("\\<Union>_" [90] 90)
+  Inter       :: i =>i                     ("\\<Inter>_" [90] 90)
   "@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)
@@ -274,4 +276,3 @@
   [(*("split", split_tr'),*)
    ("Pi",    dependent_tr' ("@PROD", "op ->")),
    ("Sigma", dependent_tr' ("@SUM", "op *"))];
-
isabelle