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 +  "ÒxÎA. B"   == "INT x:A. B"
    1.31 +  "ÓxÎA. B"   == "UN x:A. B"
    1.32 +  "ÂxÎA. P"    == "! x:A. P"
    1.33 +  "ÃxÎA. P"    == "? x:A. P"
    1.34  (* end 8bit 1 *)
    1.35  
    1.36  end