src/HOL/HOL.thy
changeset 12114 a8e860c86252
parent 12023 d982f98e0f0d
child 12161 ea4fbf26a945
     1.1 --- a/src/HOL/HOL.thy	Fri Nov 09 00:06:15 2001 +0100
     1.2 +++ b/src/HOL/HOL.thy	Fri Nov 09 00:09:47 2001 +0100
     1.3 @@ -78,11 +78,11 @@
     1.4    "="           :: "['a, 'a] => bool"                    (infix 50)
     1.5    "~="          :: "['a, 'a] => bool"                    (infix 50)
     1.6  
     1.7 -syntax (symbols)
     1.8 +syntax (xsymbols)
     1.9    Not           :: "bool => bool"                        ("\<not> _" [40] 40)
    1.10    "op &"        :: "[bool, bool] => bool"                (infixr "\<and>" 35)
    1.11    "op |"        :: "[bool, bool] => bool"                (infixr "\<or>" 30)
    1.12 -  "op -->"      :: "[bool, bool] => bool"                (infixr "\<midarrow>\<rightarrow>" 25)
    1.13 +  "op -->"      :: "[bool, bool] => bool"                (infixr "\<longrightarrow>" 25)
    1.14    "op ~="       :: "['a, 'a] => bool"                    (infix "\<noteq>" 50)
    1.15    "ALL "        :: "[idts, bool] => bool"                ("(3\<forall>_./ _)" [0, 10] 10)
    1.16    "EX "         :: "[idts, bool] => bool"                ("(3\<exists>_./ _)" [0, 10] 10)
    1.17 @@ -90,12 +90,9 @@
    1.18    "_case1"      :: "['a, 'b] => case_syn"                ("(2_ \<Rightarrow>/ _)" 10)
    1.19  (*"_case2"      :: "[case_syn, cases_syn] => cases_syn"  ("_/ \\<orelse> _")*)
    1.20  
    1.21 -syntax (symbols output)
    1.22 +syntax (xsymbols output)
    1.23    "op ~="       :: "['a, 'a] => bool"                    (infix "\<noteq>" 50)
    1.24  
    1.25 -syntax (xsymbols)
    1.26 -  "op -->"      :: "[bool, bool] => bool"                (infixr "\<longrightarrow>" 25)
    1.27 -
    1.28  syntax (HTML output)
    1.29    Not           :: "bool => bool"                        ("\<not> _" [40] 40)
    1.30  
    1.31 @@ -353,7 +350,7 @@
    1.32  
    1.33  local
    1.34  
    1.35 -syntax (symbols)
    1.36 +syntax (xsymbols)
    1.37    "op <="       :: "['a::ord, 'a] => bool"             ("op \<le>")
    1.38    "op <="       :: "['a::ord, 'a] => bool"             ("(_/ \<le> _)"  [50, 51] 50)
    1.39  
    1.40 @@ -638,7 +635,7 @@
    1.41    "_leAll"   :: "[idt, 'a, bool] => bool"   ("(3ALL _<=_./ _)" [0, 0, 10] 10)
    1.42    "_leEx"    :: "[idt, 'a, bool] => bool"   ("(3EX _<=_./ _)" [0, 0, 10] 10)
    1.43  
    1.44 -syntax (symbols)
    1.45 +syntax (xsymbols)
    1.46    "_lessAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_<_./ _)"  [0, 0, 10] 10)
    1.47    "_lessEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_<_./ _)"  [0, 0, 10] 10)
    1.48    "_leAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10)