src/FOL/IFOL.thy
changeset 12662 a9bbba3473f3
parent 12368 2af9ad81ea56
child 12875 bda60442bf02
     1.1 --- a/src/FOL/IFOL.thy	Tue Jan 08 00:03:10 2002 +0100
     1.2 +++ b/src/FOL/IFOL.thy	Tue Jan 08 00:03:42 2002 +0100
     1.3 @@ -43,7 +43,7 @@
     1.4  
     1.5  
     1.6  syntax
     1.7 -  "~="          :: "['a, 'a] => o"              (infixl 50)
     1.8 +  "_not_equal"  :: "['a, 'a] => o"              (infixl "~=" 50)
     1.9  translations
    1.10    "x ~= y"      == "~ (x = y)"
    1.11  
    1.12 @@ -54,7 +54,7 @@
    1.13    "ALL "        :: "[idts, o] => o"             ("(3\<forall>_./ _)" [0, 10] 10)
    1.14    "EX "         :: "[idts, o] => o"             ("(3\<exists>_./ _)" [0, 10] 10)
    1.15    "EX! "        :: "[idts, o] => o"             ("(3\<exists>!_./ _)" [0, 10] 10)
    1.16 -  "op ~="       :: "['a, 'a] => o"              (infixl "\<noteq>" 50)
    1.17 +  "_not_equal"  :: "['a, 'a] => o"              (infixl "\<noteq>" 50)
    1.18    "op -->"      :: "[o, o] => o"                (infixr "\<longrightarrow>" 25)
    1.19    "op <->"      :: "[o, o] => o"                (infixr "\<longleftrightarrow>" 25)
    1.20