--- 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)
--- 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)
--- 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)