Moved declaration of ~= to a syntax section
authorlcp
Tue Mar 07 13:15:25 1995 +0100 (1995-03-07)
changeset 928cb31a4e97f75
parent 927 305e7cfda869
child 929 137035296ad6
Moved declaration of ~= to a syntax section
src/FOL/IFOL.thy
     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