eliminated unnamed infixes;
authorwenzelm
Mon Feb 15 15:50:41 2010 +0100 (2010-02-15)
changeset 35128c1ad622e90e4
parent 35127 5b29c1660047
child 35129 ed24ba6f69aa
eliminated unnamed infixes;
src/FOLP/IFOLP.thy
src/LCF/LCF.thy
     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"
     2.1 --- a/src/LCF/LCF.thy	Mon Feb 15 14:04:06 2010 +0100
     2.2 +++ b/src/LCF/LCF.thy	Mon Feb 15 15:50:41 2010 +0100
     2.3 @@ -19,8 +19,8 @@
     2.4  
     2.5  typedecl tr
     2.6  typedecl void
     2.7 -typedecl ('a,'b) "*"    (infixl 6)
     2.8 -typedecl ('a,'b) "+"    (infixl 5)
     2.9 +typedecl ('a,'b) "*"    (infixl "*" 6)
    2.10 +typedecl ('a,'b) "+"    (infixl "+" 5)
    2.11  
    2.12  arities
    2.13    "fun" :: (cpo, cpo) cpo