# HG changeset patch
# User wenzelm
# Date 1010444622 -3600
# Node ID a9bbba3473f3acf294cd9086e2e4b72237e8530c
# Parent  3827cd2e9619902bd3c03db39bf2d95ee3eb1bb3
syntax "_not_equal";

diff -r 3827cd2e9619 -r a9bbba3473f3 src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Tue Jan 08 00:03:10 2002 +0100
+++ b/src/FOL/IFOL.thy	Tue Jan 08 00:03:42 2002 +0100
@@ -43,7 +43,7 @@
 
 
 syntax
-  "~="          :: "['a, 'a] => o"              (infixl 50)
+  "_not_equal"  :: "['a, 'a] => o"              (infixl "~=" 50)
 translations
   "x ~= y"      == "~ (x = y)"
 
@@ -54,7 +54,7 @@
   "ALL "        :: "[idts, o] => o"             ("(3\<forall>_./ _)" [0, 10] 10)
   "EX "         :: "[idts, o] => o"             ("(3\<exists>_./ _)" [0, 10] 10)
   "EX! "        :: "[idts, o] => o"             ("(3\<exists>!_./ _)" [0, 10] 10)
-  "op ~="       :: "['a, 'a] => o"              (infixl "\<noteq>" 50)
+  "_not_equal"  :: "['a, 'a] => o"              (infixl "\<noteq>" 50)
   "op -->"      :: "[o, o] => o"                (infixr "\<longrightarrow>" 25)
   "op <->"      :: "[o, o] => o"                (infixr "\<longleftrightarrow>" 25)
 
diff -r 3827cd2e9619 -r a9bbba3473f3 src/HOL/Modelcheck/MuckeSyn.thy
--- a/src/HOL/Modelcheck/MuckeSyn.thy	Tue Jan 08 00:03:10 2002 +0100
+++ b/src/HOL/Modelcheck/MuckeSyn.thy	Tue Jan 08 00:03:42 2002 +0100
@@ -25,7 +25,7 @@
   "op |"	:: [bool, bool] => bool			(infixr "|" 30)
   "op -->"	:: [bool, bool] => bool			(infixr "->" 25)
   "op ="        :: ['a, 'a] => bool                 ("(_ =/ _)" [51, 51] 50)
-  "op ~="       :: ['a, 'a] => bool                 ("(_ !=/ _)" [51, 51] 50)
+  "_not_equal"  :: ['a, 'a] => bool                 ("(_ !=/ _)" [51, 51] 50)
 
   "! " 		:: [idts, bool] => bool			("'((3forall _./ _)')" [0, 10] 10)
   "? "		:: [idts, bool] => bool			("'((3exists _./ _)')" [0, 10] 10)
diff -r 3827cd2e9619 -r a9bbba3473f3 src/Sequents/LK0.thy
--- a/src/Sequents/LK0.thy	Tue Jan 08 00:03:10 2002 +0100
+++ b/src/Sequents/LK0.thy	Tue Jan 08 00:03:42 2002 +0100
@@ -35,7 +35,7 @@
   Ex           :: ('a => o) => o     (binder "EX " 10)
 
 syntax
-  "~="          :: ['a, 'a] => o                (infixl 50)
+  "_not_equal" :: ['a, 'a] => o                (infixl "~=" 50)
 
 translations
   "x ~= y"      == "~ (x = y)"
@@ -49,7 +49,7 @@
   "ALL "        :: [idts, o] => o       ("(3\\<forall>_./ _)" [0, 10] 10)
   "EX "         :: [idts, o] => o       ("(3\\<exists>_./ _)" [0, 10] 10)
   "EX! "        :: [idts, o] => o       ("(3\\<exists>!_./ _)" [0, 10] 10)
-  "op ~="       :: ['a, 'a] => o        (infixl "\\<noteq>" 50)
+  "_not_equal"  :: ['a, 'a] => o        (infixl "\\<noteq>" 50)
 
 syntax (HTML output)
   Not           :: o => o               ("\\<not> _" [40] 40)