src/FOL/IFOL.thy
changeset 19363 667b5ea637dd
parent 19120 353d349740de
child 19380 b808efaa5828
     1.1 --- a/src/FOL/IFOL.thy	Sat Apr 08 22:12:02 2006 +0200
     1.2 +++ b/src/FOL/IFOL.thy	Sat Apr 08 22:51:06 2006 +0200
     1.3 @@ -45,10 +45,18 @@
     1.4    Ex1           :: "('a => o) => o"             (binder "EX! " 10)
     1.5  
     1.6  
     1.7 -abbreviation (output)
     1.8 +abbreviation
     1.9    not_equal     :: "['a, 'a] => o"              (infixl "~=" 50)
    1.10    "x ~= y == ~ (x = y)"
    1.11  
    1.12 +abbreviation (xsymbols)
    1.13 +  not_equal     :: "['a, 'a] => o"              (infixl "\<noteq>" 50)
    1.14 +  "x \<noteq> y == ~ (x = y)"
    1.15 +
    1.16 +abbreviation (HTML output)
    1.17 +  not_equal     :: "['a, 'a] => o"              (infixl "\<noteq>" 50)
    1.18 +  "not_equal == xsymbols.not_equal"
    1.19 +
    1.20  syntax (xsymbols)
    1.21    Not           :: "o => o"                     ("\<not> _" [40] 40)
    1.22    "op &"        :: "[o, o] => o"                (infixr "\<and>" 35)
    1.23 @@ -56,7 +64,6 @@
    1.24    "ALL "        :: "[idts, o] => o"             ("(3\<forall>_./ _)" [0, 10] 10)
    1.25    "EX "         :: "[idts, o] => o"             ("(3\<exists>_./ _)" [0, 10] 10)
    1.26    "EX! "        :: "[idts, o] => o"             ("(3\<exists>!_./ _)" [0, 10] 10)
    1.27 -  not_equal     :: "['a, 'a] => o"              (infixl "\<noteq>" 50)
    1.28    "op -->"      :: "[o, o] => o"                (infixr "\<longrightarrow>" 25)
    1.29    "op <->"      :: "[o, o] => o"                (infixr "\<longleftrightarrow>" 25)
    1.30  
    1.31 @@ -67,7 +74,6 @@
    1.32    "ALL "        :: "[idts, o] => o"             ("(3\<forall>_./ _)" [0, 10] 10)
    1.33    "EX "         :: "[idts, o] => o"             ("(3\<exists>_./ _)" [0, 10] 10)
    1.34    "EX! "        :: "[idts, o] => o"             ("(3\<exists>!_./ _)" [0, 10] 10)
    1.35 -  not_equal     :: "['a, 'a] => o"              (infixl "\<noteq>" 50)
    1.36  
    1.37  
    1.38  local