equal
deleted
inserted
replaced
341 |
341 |
342 |
342 |
343 subsubsection {* const serializations *} |
343 subsubsection {* const serializations *} |
344 |
344 |
345 consts_code |
345 consts_code |
346 "{}" ("[]") |
346 "{}" ("{*[]*}") |
347 "insert" ("{*insertl*}") |
347 insert ("{*insertl*}") |
348 "op Un" ("{*unionl*}") |
348 "op \<union>" ("{*unionl*}") |
349 "op Int" ("{*intersect*}") |
349 "op \<inter>" ("{*intersect*}") |
350 "minus" :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" |
350 "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{* flip subtract *}") |
351 ("{*flip subtract*}") |
351 image ("{*map_distinct*}") |
352 "image" ("{*map_distinct*}") |
352 Union ("{*unions*}") |
353 "Union" ("{*unions*}") |
353 Inter ("{*intersects*}") |
354 "Inter" ("{*intersects*}") |
354 UNION ("{*map_union*}") |
355 "UNION" ("{*map_union*}") |
355 INTER ("{*map_inter*}") |
356 "INTER" ("{*map_inter*}") |
356 Ball ("{*Blall*}") |
357 "Ball" ("{*Blall*}") |
357 Bex ("{*Blex*}") |
358 "Bex" ("{*Blex*}") |
358 filter_set ("{*filter*}") |
359 "filter_set" ("{*filter*}") |
|
360 |
359 |
361 end |
360 end |