src/HOL/HOL.thy
changeset 14565 c6dc17aab88a
parent 14444 24724afce166
child 14590 276ef51cedbf
     1.1 --- a/src/HOL/HOL.thy	Wed Apr 14 13:28:46 2004 +0200
     1.2 +++ b/src/HOL/HOL.thy	Wed Apr 14 14:13:05 2004 +0200
     1.3 @@ -102,7 +102,14 @@
     1.4    "_not_equal"  :: "['a, 'a] => bool"                    (infix "\<noteq>" 50)
     1.5  
     1.6  syntax (HTML output)
     1.7 +  "_not_equal"  :: "['a, 'a] => bool"                    (infix "\<noteq>" 50)
     1.8    Not           :: "bool => bool"                        ("\<not> _" [40] 40)
     1.9 +  "op &"        :: "[bool, bool] => bool"                (infixr "\<and>" 35)
    1.10 +  "op |"        :: "[bool, bool] => bool"                (infixr "\<or>" 30)
    1.11 +  "_not_equal"  :: "['a, 'a] => bool"                    (infix "\<noteq>" 50)
    1.12 +  "ALL "        :: "[idts, bool] => bool"                ("(3\<forall>_./ _)" [0, 10] 10)
    1.13 +  "EX "         :: "[idts, bool] => bool"                ("(3\<exists>_./ _)" [0, 10] 10)
    1.14 +  "EX! "        :: "[idts, bool] => bool"                ("(3\<exists>!_./ _)" [0, 10] 10)
    1.15  
    1.16  syntax (HOL)
    1.17    "ALL "        :: "[idts, bool] => bool"                ("(3! _./ _)" [0, 10] 10)
    1.18 @@ -639,6 +646,10 @@
    1.19    "op <="       :: "['a::ord, 'a] => bool"             ("op \<le>")
    1.20    "op <="       :: "['a::ord, 'a] => bool"             ("(_/ \<le> _)"  [50, 51] 50)
    1.21  
    1.22 +syntax (HTML output)
    1.23 +  "op <="       :: "['a::ord, 'a] => bool"             ("op \<le>")
    1.24 +  "op <="       :: "['a::ord, 'a] => bool"             ("(_/ \<le> _)"  [50, 51] 50)
    1.25 +
    1.26  
    1.27  lemma Not_eq_iff: "((~P) = (~Q)) = (P = Q)"
    1.28  by blast
    1.29 @@ -1056,6 +1067,12 @@
    1.30    "_leAll"   :: "[idt, 'a, bool] => bool"   ("(3! _<=_./ _)" [0, 0, 10] 10)
    1.31    "_leEx"    :: "[idt, 'a, bool] => bool"   ("(3? _<=_./ _)" [0, 0, 10] 10)
    1.32  
    1.33 +syntax (HTML output)
    1.34 +  "_lessAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_<_./ _)"  [0, 0, 10] 10)
    1.35 +  "_lessEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_<_./ _)"  [0, 0, 10] 10)
    1.36 +  "_leAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10)
    1.37 +  "_leEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10)
    1.38 +
    1.39  translations
    1.40   "ALL x<y. P"   =>  "ALL x. x < y --> P"
    1.41   "EX x<y. P"    =>  "EX x. x < y  & P"