| changeset 70009 | 435fb018e8ee |
| parent 63167 | 0909deb8059b |
| 70008:7aaebfcf3134 | 70009:435fb018e8ee |
|---|---|
26 lift_definition insert :: "'a => 'a set => 'a set" is "\<lambda> x P y. y = x \<or> P y" . |
26 lift_definition insert :: "'a => 'a set => 'a set" is "\<lambda> x P y. y = x \<or> P y" . |
27 |
27 |
28 term "Lift_Set.insert" |
28 term "Lift_Set.insert" |
29 thm Lift_Set.insert_def |
29 thm Lift_Set.insert_def |
30 |
30 |
31 export_code empty insert in SML |
31 export_code empty insert in SML file_prefix set |
32 |
32 |
33 end |
33 end |