30 notation (xsymbols) |
30 notation (xsymbols) |
31 "lesub" ("(_ /\<sqsubseteq>\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and |
31 "lesub" ("(_ /\<sqsubseteq>\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and |
32 "lesssub" ("(_ /\<sqsubset>\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and |
32 "lesssub" ("(_ /\<sqsubset>\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and |
33 "plussub" ("(_ /\<squnion>\<^bsub>_\<^esub> _)" [65, 0, 66] 65) |
33 "plussub" ("(_ /\<squnion>\<^bsub>_\<^esub> _)" [65, 0, 66] 65) |
34 (*<*) |
34 (*<*) |
35 syntax |
35 (* allow \<sub> instead of \<bsub>..\<esub> *) |
36 (* allow \<sub> instead of \<bsub>..\<esub> *) |
36 |
37 "_lesub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubseteq>\<^sub>_ _)" [50, 1000, 51] 50) |
37 abbreviation (input) |
38 "_lesssub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubset>\<^sub>_ _)" [50, 1000, 51] 50) |
38 lesub1 :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubseteq>\<^sub>_ _)" [50, 1000, 51] 50) |
39 "_plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /\<squnion>\<^sub>_ _)" [65, 1000, 66] 65) |
39 where "x \<sqsubseteq>\<^sub>r y == x \<sqsubseteq>\<^bsub>r\<^esub> y" |
40 |
40 |
41 translations |
41 abbreviation (input) |
42 "x \<sqsubseteq>\<^sub>r y" => "x \<sqsubseteq>\<^bsub>r\<^esub> y" |
42 lesssub1 :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubset>\<^sub>_ _)" [50, 1000, 51] 50) |
43 "x \<sqsubset>\<^sub>r y" => "x \<sqsubset>\<^bsub>r\<^esub> y" |
43 where "x \<sqsubset>\<^sub>r y == x \<sqsubset>\<^bsub>r\<^esub> y" |
44 "x \<squnion>\<^sub>f y" => "x \<squnion>\<^bsub>f\<^esub> y" |
44 |
|
45 abbreviation (input) |
|
46 plussub1 :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /\<squnion>\<^sub>_ _)" [65, 1000, 66] 65) |
|
47 where "x \<squnion>\<^sub>f y == x \<squnion>\<^bsub>f\<^esub> y" |
45 (*>*) |
48 (*>*) |
46 |
49 |
47 defs |
50 defs |
48 lesub_def: "x \<sqsubseteq>\<^sub>r y \<equiv> r x y" |
51 lesub_def: "x \<sqsubseteq>\<^sub>r y \<equiv> r x y" |
49 lesssub_def: "x \<sqsubset>\<^sub>r y \<equiv> x \<sqsubseteq>\<^sub>r y \<and> x \<noteq> y" |
52 lesssub_def: "x \<sqsubset>\<^sub>r y \<equiv> x \<sqsubseteq>\<^sub>r y \<and> x \<noteq> y" |