a little tidying; also FIXED BAD TYPE in INTER1, UNION1
authorpaulson
Thu Aug 26 11:32:39 1999 +0200 (1999-08-26)
changeset 73589e95b846ad42
parent 7357 d0e16da40ea2
child 7359 98a2afab3f86
a little tidying; also FIXED BAD TYPE in INTER1, UNION1
src/HOL/Set.thy
     1.1 --- a/src/HOL/Set.thy	Wed Aug 25 20:49:02 1999 +0200
     1.2 +++ b/src/HOL/Set.thy	Thu Aug 26 11:32:39 1999 +0200
     1.3 @@ -56,8 +56,8 @@
     1.4  
     1.5    (* Big Intersection / Union *)
     1.6  
     1.7 -  INTER1        :: [pttrns, 'a => 'b set] => 'b set   ("(3INT _./ _)" 10)
     1.8 -  UNION1        :: [pttrns, 'a => 'b set] => 'b set   ("(3UN _./ _)" 10)
     1.9 +  "@INTER1"     :: [pttrns, 'b set] => 'b set   ("(3INT _./ _)" 10)
    1.10 +  "@UNION1"     :: [pttrns, 'b set] => 'b set   ("(3UN _./ _)" 10)
    1.11  
    1.12    "@INTER"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3INT _:_./ _)" 10)
    1.13    "@UNION"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3UN _:_./ _)" 10)
    1.14 @@ -104,8 +104,8 @@
    1.15    "op ~:"       :: ['a, 'a set] => bool               ("(_/ \\<notin> _)" [50, 51] 50)
    1.16    "UN "         :: [idts, bool] => bool               ("(3\\<Union> _./ _)" 10)
    1.17    "INT "        :: [idts, bool] => bool               ("(3\\<Inter> _./ _)" 10)
    1.18 -  "UNION1"      :: [pttrn, 'b set] => 'b set          ("(3\\<Union> _./ _)" 10)
    1.19 -  "INTER1"      :: [pttrn, 'b set] => 'b set          ("(3\\<Inter> _./ _)" 10)
    1.20 +  "@UNION1"     :: [pttrn, 'b set] => 'b set          ("(3\\<Union> _./ _)" 10)
    1.21 +  "@INTER1"     :: [pttrn, 'b set] => 'b set          ("(3\\<Inter> _./ _)" 10)
    1.22    "@UNION"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3\\<Union> _\\<in>_./ _)" 10)
    1.23    "@INTER"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3\\<Inter> _\\<in>_./ _)" 10)
    1.24    Union         :: (('a set) set) => 'a set           ("\\<Union> _" [90] 90)