18 consts |
18 consts |
19 "lesub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" |
19 "lesub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" |
20 "lesssub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" |
20 "lesssub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" |
21 "plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" |
21 "plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" |
22 (*<*) |
22 (*<*) |
23 notation |
23 notation (ASCII) |
24 "lesub" ("(_ /<='__ _)" [50, 1000, 51] 50) and |
24 "lesub" ("(_ /<='__ _)" [50, 1000, 51] 50) and |
25 "lesssub" ("(_ /<'__ _)" [50, 1000, 51] 50) and |
25 "lesssub" ("(_ /<'__ _)" [50, 1000, 51] 50) and |
26 "plussub" ("(_ /+'__ _)" [65, 1000, 66] 65) |
26 "plussub" ("(_ /+'__ _)" [65, 1000, 66] 65) |
27 (*>*) |
27 (*>*) |
28 notation (xsymbols) |
28 notation |
29 "lesub" ("(_ /\<sqsubseteq>\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and |
29 "lesub" ("(_ /\<sqsubseteq>\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and |
30 "lesssub" ("(_ /\<sqsubset>\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and |
30 "lesssub" ("(_ /\<sqsubset>\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and |
31 "plussub" ("(_ /\<squnion>\<^bsub>_\<^esub> _)" [65, 0, 66] 65) |
31 "plussub" ("(_ /\<squnion>\<^bsub>_\<^esub> _)" [65, 0, 66] 65) |
32 (*<*) |
32 (*<*) |
33 (* allow \<sub> instead of \<bsub>..\<esub> *) |
33 (* allow \<sub> instead of \<bsub>..\<esub> *) |