equal
deleted
inserted
replaced
283 INTER \<equiv> map_inter |
283 INTER \<equiv> map_inter |
284 Ball \<equiv> Blall |
284 Ball \<equiv> Blall |
285 Bex \<equiv> Blex |
285 Bex \<equiv> Blex |
286 |
286 |
287 code_gen "{}" insert "op \<union>" "op \<inter>" "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" |
287 code_gen "{}" insert "op \<union>" "op \<inter>" "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" |
288 image Union Inter UNION INTER Ball Bex (SML -) |
288 image Union Inter UNION INTER Ball Bex (SML *) |
289 |
289 |
290 |
290 |
291 subsection {* type serializations *} |
291 subsection {* type serializations *} |
292 |
292 |
293 types_code |
293 types_code |