src/HOL/HOL.thy
changeset 12650 fbc17f1e746b
parent 12633 ad9277743664
child 12892 a0b2acb7d6fa
     1.1 --- a/src/HOL/HOL.thy	Sun Jan 06 16:50:31 2002 +0100
     1.2 +++ b/src/HOL/HOL.thy	Sun Jan 06 16:51:04 2002 +0100
     1.3 @@ -56,7 +56,7 @@
     1.4    case_syn  cases_syn
     1.5  
     1.6  syntax
     1.7 -  ~=            :: "['a, 'a] => bool"                    (infixl 50)
     1.8 +  "_not_equal"  :: "['a, 'a] => bool"                    (infixl "~=" 50)
     1.9    "_The"        :: "[pttrn, bool] => 'a"                 ("(3THE _./ _)" [0, 10] 10)
    1.10  
    1.11    "_bind"       :: "[pttrn, 'a] => letbind"              ("(2_ =/ _)" 10)
    1.12 @@ -77,14 +77,14 @@
    1.13  
    1.14  syntax (output)
    1.15    "="           :: "['a, 'a] => bool"                    (infix 50)
    1.16 -  "~="          :: "['a, 'a] => bool"                    (infix 50)
    1.17 +  "_not_equal"  :: "['a, 'a] => bool"                    (infix "~=" 50)
    1.18  
    1.19  syntax (xsymbols)
    1.20    Not           :: "bool => bool"                        ("\<not> _" [40] 40)
    1.21    "op &"        :: "[bool, bool] => bool"                (infixr "\<and>" 35)
    1.22    "op |"        :: "[bool, bool] => bool"                (infixr "\<or>" 30)
    1.23    "op -->"      :: "[bool, bool] => bool"                (infixr "\<longrightarrow>" 25)
    1.24 -  "op ~="       :: "['a, 'a] => bool"                    (infix "\<noteq>" 50)
    1.25 +  "_not_equal"  :: "['a, 'a] => bool"                    (infix "\<noteq>" 50)
    1.26    "ALL "        :: "[idts, bool] => bool"                ("(3\<forall>_./ _)" [0, 10] 10)
    1.27    "EX "         :: "[idts, bool] => bool"                ("(3\<exists>_./ _)" [0, 10] 10)
    1.28    "EX! "        :: "[idts, bool] => bool"                ("(3\<exists>!_./ _)" [0, 10] 10)
    1.29 @@ -92,7 +92,7 @@
    1.30  (*"_case2"      :: "[case_syn, cases_syn] => cases_syn"  ("_/ \\<orelse> _")*)
    1.31  
    1.32  syntax (xsymbols output)
    1.33 -  "op ~="       :: "['a, 'a] => bool"                    (infix "\<noteq>" 50)
    1.34 +  "_not_equal"  :: "['a, 'a] => bool"                    (infix "\<noteq>" 50)
    1.35  
    1.36  syntax (HTML output)
    1.37    Not           :: "bool => bool"                        ("\<not> _" [40] 40)