Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Moved declaration of ~= to a syntax section
authorlcp
Tue, 07 Mar 1995 13:15:25 +0100
changeset 928 cb31a4e97f75
parent 927 305e7cfda869
child 929 137035296ad6
Moved declaration of ~= to a syntax section
src/FOL/IFOL.thy file | annotate | diff | comparison | revisions 
--- 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)"
isabelle