equal
deleted
inserted
replaced
178 (infixl \<open>\<union>\<natural>\<close> 65) where |
178 (infixl \<open>\<union>\<natural>\<close> 65) where |
179 "xs \<union>\<natural> ys == convex_plus\<cdot>xs\<cdot>ys" |
179 "xs \<union>\<natural> ys == convex_plus\<cdot>xs\<cdot>ys" |
180 |
180 |
181 syntax |
181 syntax |
182 "_convex_pd" :: "args \<Rightarrow> logic" (\<open>(\<open>indent=1 notation=\<open>mixfix convex_pd enumeration\<close>\<close>{_}\<natural>)\<close>) |
182 "_convex_pd" :: "args \<Rightarrow> logic" (\<open>(\<open>indent=1 notation=\<open>mixfix convex_pd enumeration\<close>\<close>{_}\<natural>)\<close>) |
183 syntax_consts |
|
184 convex_add |
|
185 translations |
183 translations |
186 "{x,xs}\<natural>" == "{x}\<natural> \<union>\<natural> {xs}\<natural>" |
184 "{x,xs}\<natural>" == "{x}\<natural> \<union>\<natural> {xs}\<natural>" |
187 "{x}\<natural>" == "CONST convex_unit\<cdot>x" |
185 "{x}\<natural>" == "CONST convex_unit\<cdot>x" |
188 |
186 |
189 lemma convex_unit_Rep_compact_basis [simp]: |
187 lemma convex_unit_Rep_compact_basis [simp]: |