src/HOL/Orderings.thy
changeset 61378 3e04c9ca001a
parent 61169 4de9ff3ea29a
child 61605 1bf7b186542e
equal deleted inserted replaced
61377:517feb558c77 61378:3e04c9ca001a
    97   less_eq  ("(_/ <= _)" [51, 51] 50) and
    97   less_eq  ("(_/ <= _)" [51, 51] 50) and
    98   less  ("op <") and
    98   less  ("op <") and
    99   less  ("(_/ < _)"  [51, 51] 50)
    99   less  ("(_/ < _)"  [51, 51] 50)
   100   
   100   
   101 notation (xsymbols)
   101 notation (xsymbols)
   102   less_eq  ("op \<le>") and
       
   103   less_eq  ("(_/ \<le> _)"  [51, 51] 50)
       
   104 
       
   105 notation (HTML output)
       
   106   less_eq  ("op \<le>") and
   102   less_eq  ("op \<le>") and
   107   less_eq  ("(_/ \<le> _)"  [51, 51] 50)
   103   less_eq  ("(_/ \<le> _)"  [51, 51] 50)
   108 
   104 
   109 abbreviation (input)
   105 abbreviation (input)
   110   greater_eq  (infix ">=" 50) where
   106   greater_eq  (infix ">=" 50) where
   679   "_All_less" :: "[idt, 'a, bool] => bool"    ("(3! _<_./ _)"  [0, 0, 10] 10)
   675   "_All_less" :: "[idt, 'a, bool] => bool"    ("(3! _<_./ _)"  [0, 0, 10] 10)
   680   "_Ex_less" :: "[idt, 'a, bool] => bool"    ("(3? _<_./ _)"  [0, 0, 10] 10)
   676   "_Ex_less" :: "[idt, 'a, bool] => bool"    ("(3? _<_./ _)"  [0, 0, 10] 10)
   681   "_All_less_eq" :: "[idt, 'a, bool] => bool"    ("(3! _<=_./ _)" [0, 0, 10] 10)
   677   "_All_less_eq" :: "[idt, 'a, bool] => bool"    ("(3! _<=_./ _)" [0, 0, 10] 10)
   682   "_Ex_less_eq" :: "[idt, 'a, bool] => bool"    ("(3? _<=_./ _)" [0, 0, 10] 10)
   678   "_Ex_less_eq" :: "[idt, 'a, bool] => bool"    ("(3? _<=_./ _)" [0, 0, 10] 10)
   683 
   679 
   684 syntax (HTML output)
       
   685   "_All_less" :: "[idt, 'a, bool] => bool"    ("(3\<forall>_<_./ _)"  [0, 0, 10] 10)
       
   686   "_Ex_less" :: "[idt, 'a, bool] => bool"    ("(3\<exists>_<_./ _)"  [0, 0, 10] 10)
       
   687   "_All_less_eq" :: "[idt, 'a, bool] => bool"    ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10)
       
   688   "_Ex_less_eq" :: "[idt, 'a, bool] => bool"    ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10)
       
   689 
       
   690   "_All_greater" :: "[idt, 'a, bool] => bool"    ("(3\<forall>_>_./ _)"  [0, 0, 10] 10)
       
   691   "_Ex_greater" :: "[idt, 'a, bool] => bool"    ("(3\<exists>_>_./ _)"  [0, 0, 10] 10)
       
   692   "_All_greater_eq" :: "[idt, 'a, bool] => bool"    ("(3\<forall>_\<ge>_./ _)" [0, 0, 10] 10)
       
   693   "_Ex_greater_eq" :: "[idt, 'a, bool] => bool"    ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10)
       
   694 
       
   695 translations
   680 translations
   696   "ALL x<y. P"   =>  "ALL x. x < y \<longrightarrow> P"
   681   "ALL x<y. P"   =>  "ALL x. x < y \<longrightarrow> P"
   697   "EX x<y. P"    =>  "EX x. x < y \<and> P"
   682   "EX x<y. P"    =>  "EX x. x < y \<and> P"
   698   "ALL x<=y. P"  =>  "ALL x. x <= y \<longrightarrow> P"
   683   "ALL x<=y. P"  =>  "ALL x. x <= y \<longrightarrow> P"
   699   "EX x<=y. P"   =>  "EX x. x <= y \<and> P"
   684   "EX x<=y. P"   =>  "EX x. x <= y \<and> P"