src/HOL/Set.thy
changeset 1674 33aff4d854e4
parent 1672 2c109cd2fdd0
child 1883 00b4b6992945
     1.1 --- a/src/HOL/Set.thy	Tue Apr 23 16:58:57 1996 +0200
     1.2 +++ b/src/HOL/Set.thy	Tue Apr 23 17:01:51 1996 +0200
     1.3 @@ -104,33 +104,6 @@
     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