syntax "_not_equal";
authorwenzelm
Tue Jan 08 00:03:42 2002 +0100 (2002-01-08)
changeset 12662a9bbba3473f3
parent 12661 3827cd2e9619
child 12663 d33033205e2f
syntax "_not_equal";
src/FOL/IFOL.thy
src/HOL/Modelcheck/MuckeSyn.thy
src/Sequents/LK0.thy
     1.1 --- a/src/FOL/IFOL.thy	Tue Jan 08 00:03:10 2002 +0100
     1.2 +++ b/src/FOL/IFOL.thy	Tue Jan 08 00:03:42 2002 +0100
     1.3 @@ -43,7 +43,7 @@
     1.4  
     1.5  
     1.6  syntax
     1.7 -  "~="          :: "['a, 'a] => o"              (infixl 50)
     1.8 +  "_not_equal"  :: "['a, 'a] => o"              (infixl "~=" 50)
     1.9  translations
    1.10    "x ~= y"      == "~ (x = y)"
    1.11  
    1.12 @@ -54,7 +54,7 @@
    1.13    "ALL "        :: "[idts, o] => o"             ("(3\<forall>_./ _)" [0, 10] 10)
    1.14    "EX "         :: "[idts, o] => o"             ("(3\<exists>_./ _)" [0, 10] 10)
    1.15    "EX! "        :: "[idts, o] => o"             ("(3\<exists>!_./ _)" [0, 10] 10)
    1.16 -  "op ~="       :: "['a, 'a] => o"              (infixl "\<noteq>" 50)
    1.17 +  "_not_equal"  :: "['a, 'a] => o"              (infixl "\<noteq>" 50)
    1.18    "op -->"      :: "[o, o] => o"                (infixr "\<longrightarrow>" 25)
    1.19    "op <->"      :: "[o, o] => o"                (infixr "\<longleftrightarrow>" 25)
    1.20  
     2.1 --- a/src/HOL/Modelcheck/MuckeSyn.thy	Tue Jan 08 00:03:10 2002 +0100
     2.2 +++ b/src/HOL/Modelcheck/MuckeSyn.thy	Tue Jan 08 00:03:42 2002 +0100
     2.3 @@ -25,7 +25,7 @@
     2.4    "op |"	:: [bool, bool] => bool			(infixr "|" 30)
     2.5    "op -->"	:: [bool, bool] => bool			(infixr "->" 25)
     2.6    "op ="        :: ['a, 'a] => bool                 ("(_ =/ _)" [51, 51] 50)
     2.7 -  "op ~="       :: ['a, 'a] => bool                 ("(_ !=/ _)" [51, 51] 50)
     2.8 +  "_not_equal"  :: ['a, 'a] => bool                 ("(_ !=/ _)" [51, 51] 50)
     2.9  
    2.10    "! " 		:: [idts, bool] => bool			("'((3forall _./ _)')" [0, 10] 10)
    2.11    "? "		:: [idts, bool] => bool			("'((3exists _./ _)')" [0, 10] 10)
     3.1 --- a/src/Sequents/LK0.thy	Tue Jan 08 00:03:10 2002 +0100
     3.2 +++ b/src/Sequents/LK0.thy	Tue Jan 08 00:03:42 2002 +0100
     3.3 @@ -35,7 +35,7 @@
     3.4    Ex           :: ('a => o) => o     (binder "EX " 10)
     3.5  
     3.6  syntax
     3.7 -  "~="          :: ['a, 'a] => o                (infixl 50)
     3.8 +  "_not_equal" :: ['a, 'a] => o                (infixl "~=" 50)
     3.9  
    3.10  translations
    3.11    "x ~= y"      == "~ (x = y)"
    3.12 @@ -49,7 +49,7 @@
    3.13    "ALL "        :: [idts, o] => o       ("(3\\<forall>_./ _)" [0, 10] 10)
    3.14    "EX "         :: [idts, o] => o       ("(3\\<exists>_./ _)" [0, 10] 10)
    3.15    "EX! "        :: [idts, o] => o       ("(3\\<exists>!_./ _)" [0, 10] 10)
    3.16 -  "op ~="       :: ['a, 'a] => o        (infixl "\\<noteq>" 50)
    3.17 +  "_not_equal"  :: ['a, 'a] => o        (infixl "\\<noteq>" 50)
    3.18  
    3.19  syntax (HTML output)
    3.20    Not           :: o => o               ("\\<not> _" [40] 40)