src/HOL/Set.thy
changeset 1672 2c109cd2fdd0
parent 1531 e5eb247ad13c
child 1674 33aff4d854e4
     1.1 --- a/src/HOL/Set.thy	Tue Apr 23 16:44:22 1996 +0200
     1.2 +++ b/src/HOL/Set.thy	Tue Apr 23 16:58:21 1996 +0200
     1.3 @@ -104,6 +104,33 @@
     1.4    surj_def      "surj(f)        == ! y. ? x. y=f(x)"
     1.5  
     1.6  (* start 8bit 1 *)
     1.7 +syntax
     1.8 +  ""		:: "['a set, 'a set] => 'a set"       (infixl 70)
     1.9 +  ""		:: "['a set, 'a set] => 'a set"       (infixl 65)
    1.10 +  ""		:: "['a, 'a set] => bool"             (infixl 50)
    1.11 +  ""		:: "['a, 'a set] => bool"             (infixl 50)
    1.12 +  GUnion	:: "(('a set)set) => 'a set"          ("_" [90] 90)
    1.13 +  GInter	:: "(('a set)set) => 'a set"          ("_" [90] 90)
    1.14 +  GUNION1       :: "['a => 'b set] => 'b set"         (binder " " 10)
    1.15 +  GINTER1       :: "['a => 'b set] => 'b set"         (binder " " 10)
    1.16 +  GINTER	:: "[pttrn, 'a set, 'b set] => 'b set"  ("(3 __./ _)" 10)
    1.17 +  GUNION	:: "[pttrn, 'a set, 'b set] => 'b set"  ("(3 __./ _)" 10)
    1.18 +  GBall		:: "[pttrn, 'a set, bool] => bool"      ("(3 __./ _)" 10)
    1.19 +  GBex		:: "[pttrn, 'a set, bool] => bool"      ("(3 __./ _)" 10)
    1.20 +
    1.21 +translations
    1.22 +  "x  y"      == "(x : y)"
    1.23 +  "x  y"      == "(x : y)"
    1.24 +  "x  y"      == "x Int y"
    1.25 +  "x  y"      == "x Un  y"
    1.26 +  "X"        == "Inter X" 
    1.27 +  "X"        == "Union X"
    1.28 +  "x.A"      == "INT x.A"
    1.29 +  "x.A"      == "UN x.A"
    1.30 +  "xA. B"   == "INT x:A. B"
    1.31 +  "xA. B"   == "UN x:A. B"
    1.32 +  "xA. P"    == "! x:A. P"
    1.33 +  "xA. P"    == "? x:A. P"
    1.34  (* end 8bit 1 *)
    1.35  
    1.36  end