src/FOL/IFOL.thy
changeset 928 cb31a4e97f75
parent 278 523518f44286
child 1268 f6ef556b3ede
     1.1 --- a/src/FOL/IFOL.thy	Fri Mar 03 12:48:06 1995 +0100
     1.2 +++ b/src/FOL/IFOL.thy	Tue Mar 07 13:15:25 1995 +0100
     1.3 @@ -29,7 +29,6 @@
     1.4    (* Connectives *)
     1.5  
     1.6    "="           :: "['a, 'a] => o"              (infixl 50)
     1.7 -  "~="          :: "['a, 'a] => o"              ("(_ ~=/ _)" [50, 51] 50)
     1.8  
     1.9    Not           :: "o => o"                     ("~ _" [40] 40)
    1.10    "&"           :: "[o, o] => o"                (infixr 35)
    1.11 @@ -44,6 +43,9 @@
    1.12    Ex1           :: "('a => o) => o"             (binder "EX! " 10)
    1.13  
    1.14  
    1.15 +syntax
    1.16 +  "~="          :: "['a, 'a] => o"              (infixl 50)
    1.17 +
    1.18  translations
    1.19    "x ~= y"      == "~ (x = y)"
    1.20