symbol names changes;
authorwenzelm
Wed Nov 27 16:42:48 1996 +0100 (1996-11-27)
changeset 2257c8154379738c
parent 2256 e9326ab92fbc
child 2258 8ad8ee759d9f
symbol names changes;
src/FOL/IFOL.thy
     1.1 --- a/src/FOL/IFOL.thy	Wed Nov 27 16:41:56 1996 +0100
     1.2 +++ b/src/FOL/IFOL.thy	Wed Nov 27 16:42:48 1996 +0100
     1.3 @@ -43,22 +43,23 @@
     1.4    Ex1           :: ('a => o) => o               (binder "EX! " 10)
     1.5  
     1.6  
     1.7 +
     1.8  syntax
     1.9    "~="          :: ['a, 'a] => o                (infixl 50)
    1.10  
    1.11  translations
    1.12    "x ~= y"      == "~ (x = y)"
    1.13  
    1.14 -syntax (symbolfont)
    1.15 -  Not           :: o => o                       ("\\{neg} _" [40] 40)
    1.16 -  "op &"        :: [o, o] => o                  (infixr "\\{vee}" 35)
    1.17 -  "op |"        :: [o, o] => o                  (infixr "\\{wedge}" 30)
    1.18 -  "op -->"      :: [o, o] => o                  (infixr "\\{midarrow}\\{rightarrow}" 25)
    1.19 -  "op <->"      :: [o, o] => o                  (infixr "\\{leftarrow}\\{rightarrow}" 25)
    1.20 -  "ALL "        :: [idts, o] => o               ("(3\\{forall}_./ _)" 10)
    1.21 -  "EX "         :: [idts, o] => o               ("(3\\{exists}_./ _)" 10)
    1.22 -  "EX! "        :: [idts, o] => o               ("(3\\{exists}!_./ _)" 10)
    1.23 -  "op ~="       :: ['a, 'a] => o                (infixl "\\{noteq}" 50)
    1.24 +syntax (symbols)
    1.25 +  Not           :: o => o                       ("\\<not> _" [40] 40)
    1.26 +  "op &"        :: [o, o] => o                  (infixr "\\<and>" 35)
    1.27 +  "op |"        :: [o, o] => o                  (infixr "\\<or>" 30)
    1.28 +  "op -->"      :: [o, o] => o                  (infixr "\\<midarrow>\\<rightarrow>" 25)
    1.29 +  "op <->"      :: [o, o] => o                  (infixr "\\<leftarrow>\\<rightarrow>" 25)
    1.30 +  "ALL "        :: [idts, o] => o               ("(3\\<forall>_./ _)" 10)
    1.31 +  "EX "         :: [idts, o] => o               ("(3\\<exists>_./ _)" 10)
    1.32 +  "EX! "        :: [idts, o] => o               ("(3\\<exists>!_./ _)" 10)
    1.33 +  "op ~="       :: ['a, 'a] => o                (infixl "\\<noteq>" 50)
    1.34  
    1.35  
    1.36  rules