src/FOLP/IFOLP.thy
changeset 35128 c1ad622e90e4
parent 35113 1a0c129bb2e0
child 36319 8feb2c4bef1a
     1.1 --- a/src/FOLP/IFOLP.thy	Mon Feb 15 14:04:06 2010 +0100
     1.2 +++ b/src/FOLP/IFOLP.thy	Mon Feb 15 15:50:41 2010 +0100
     1.3 @@ -26,14 +26,14 @@
     1.4   EqProof        ::   "[p,p,o]=>prop"    ("(3_ /= _ :/ _)" [10,10,10] 5)
     1.5  
     1.6        (*** Logical Connectives -- Type Formers ***)
     1.7 - "="            ::      "['a,'a] => o"  (infixl 50)
     1.8 + "op ="         ::      "['a,'a] => o"  (infixl "=" 50)
     1.9   True           ::      "o"
    1.10   False          ::      "o"
    1.11   Not            ::      "o => o"        ("~ _" [40] 40)
    1.12 - "&"            ::      "[o,o] => o"    (infixr 35)
    1.13 - "|"            ::      "[o,o] => o"    (infixr 30)
    1.14 - "-->"          ::      "[o,o] => o"    (infixr 25)
    1.15 - "<->"          ::      "[o,o] => o"    (infixr 25)
    1.16 + "op &"         ::      "[o,o] => o"    (infixr "&" 35)
    1.17 + "op |"         ::      "[o,o] => o"    (infixr "|" 30)
    1.18 + "op -->"       ::      "[o,o] => o"    (infixr "-->" 25)
    1.19 + "op <->"       ::      "[o,o] => o"    (infixr "<->" 25)
    1.20        (*Quantifiers*)
    1.21   All            ::      "('a => o) => o"        (binder "ALL " 10)
    1.22   Ex             ::      "('a => o) => o"        (binder "EX " 10)
    1.23 @@ -53,9 +53,9 @@
    1.24   inr            :: "p=>p"
    1.25   when           :: "[p, p=>p, p=>p]=>p"
    1.26   lambda         :: "(p => p) => p"      (binder "lam " 55)
    1.27 - "`"            :: "[p,p]=>p"           (infixl 60)
    1.28 + "op `"         :: "[p,p]=>p"           (infixl "`" 60)
    1.29   alll           :: "['a=>p]=>p"         (binder "all " 55)
    1.30 - "^"            :: "[p,'a]=>p"          (infixl 55)
    1.31 + "op ^"         :: "[p,'a]=>p"          (infixl "^" 55)
    1.32   exists         :: "['a,p]=>p"          ("(1[_,/_])")
    1.33   xsplit         :: "[p,['a,p]=>p]=>p"
    1.34   ideq           :: "'a=>p"