changeset 928 | cb31a4e97f75 |
parent 278 | 523518f44286 |
child 1268 | f6ef556b3ede |
--- a/src/FOL/IFOL.thy Fri Mar 03 12:48:06 1995 +0100 +++ b/src/FOL/IFOL.thy Tue Mar 07 13:15:25 1995 +0100 @@ -29,7 +29,6 @@ (* Connectives *) "=" :: "['a, 'a] => o" (infixl 50) - "~=" :: "['a, 'a] => o" ("(_ ~=/ _)" [50, 51] 50) Not :: "o => o" ("~ _" [40] 40) "&" :: "[o, o] => o" (infixr 35) @@ -44,6 +43,9 @@ Ex1 :: "('a => o) => o" (binder "EX! " 10) +syntax + "~=" :: "['a, 'a] => o" (infixl 50) + translations "x ~= y" == "~ (x = y)"