src/Tools/8bit/isa-patches/HOL/Set.p
changeset 11390 735bf767833a
parent 11389 55e2aef8909b
child 11391 e8638d07fdee
equal deleted inserted replaced
11389:55e2aef8909b 11390:735bf767833a
     1 syntax
       
     2   "Ð"		:: "['a set, 'a set] => 'a set"       (infixl 70)
       
     3   "Ñ"		:: "['a set, 'a set] => 'a set"       (infixl 65)
       
     4   "Î"		:: "['a, 'a set] => bool"             (infixl 50)
       
     5   "ñ"		:: "['a, 'a set] => bool"             (infixl 50)
       
     6   GUnion	:: "(('a set)set) => 'a set"          ("Ó_" [90] 90)
       
     7   GInter	:: "(('a set)set) => 'a set"          ("Ò_" [90] 90)
       
     8   GUNION1       :: "['a => 'b set] => 'b set"         (binder "Ó " 10)
       
     9   GINTER1       :: "['a => 'b set] => 'b set"         (binder "Ò " 10)
       
    10   GINTER	:: "[pttrn, 'a set, 'b set] => 'b set"  ("(3Ò _Î_./ _)" 10)
       
    11   GUNION	:: "[pttrn, 'a set, 'b set] => 'b set"  ("(3Ó _Î_./ _)" 10)
       
    12   GBall		:: "[pttrn, 'a set, bool] => bool"      ("(3Â _Î_./ _)" 10)
       
    13   GBex		:: "[pttrn, 'a set, bool] => bool"      ("(3Ã _Î_./ _)" 10)
       
    14 
       
    15 translations
       
    16   "x ñ y"      == "¿(x : y)"
       
    17   "x Î y"      == "(x : y)"
       
    18   "x Ð y"      == "x Int y"
       
    19   "x Ñ y"      == "x Un  y"
       
    20   "ÒX"        == "Inter X" 
       
    21   "ÓX"        == "Union X"
       
    22   "Òx.A"      == "INT x.A"
       
    23   "Óx.A"      == "UN x.A"
       
    24   "ÒxÎA. B"   == "INT x:A. B"
       
    25   "ÓxÎA. B"   == "UN x:A. B"
       
    26   "ÂxÎA. P"    == "! x:A. P"
       
    27   "ÃxÎA. P"    == "? x:A. P"