src/FOLP/IFOLP.thy
changeset 2714 b0fbdfbbad66
parent 1477 4c51ab632cda
child 3836 f1a1817659e6
equal deleted inserted replaced
2713:7231c1e89706 2714:b0fbdfbbad66
    26  EqProof        ::   "[p,p,o]=>prop"    ("(3_ /= _ :/ _)" [10,10,10] 5)
    26  EqProof        ::   "[p,p,o]=>prop"    ("(3_ /= _ :/ _)" [10,10,10] 5)
    27         
    27         
    28       (*** Logical Connectives -- Type Formers ***)
    28       (*** Logical Connectives -- Type Formers ***)
    29  "="            ::      "['a,'a] => o"  (infixl 50)
    29  "="            ::      "['a,'a] => o"  (infixl 50)
    30  True,False     ::      "o"
    30  True,False     ::      "o"
    31  "Not"          ::      "o => o"        ("~ _" [40] 40)
    31  Not            ::      "o => o"        ("~ _" [40] 40)
    32  "&"            ::      "[o,o] => o"    (infixr 35)
    32  "&"            ::      "[o,o] => o"    (infixr 35)
    33  "|"            ::      "[o,o] => o"    (infixr 30)
    33  "|"            ::      "[o,o] => o"    (infixr 30)
    34  "-->"          ::      "[o,o] => o"    (infixr 25)
    34  "-->"          ::      "[o,o] => o"    (infixr 25)
    35  "<->"          ::      "[o,o] => o"    (infixr 25)
    35  "<->"          ::      "[o,o] => o"    (infixr 25)
    36       (*Quantifiers*)
    36       (*Quantifiers*)