| changeset 18772 | f0dd51087eb3 |
| parent 18757 | f0d901bc0686 |
| child 18851 | 9502ce541f01 |
| 18771:63efe00371af | 18772:f0dd51087eb3 |
|---|---|
60 "Ball" ("\<module>Ball") |
60 "Ball" ("\<module>Ball") |
61 attach {* |
61 attach {* |
62 fun Ball S P = Library.forall P S; |
62 fun Ball S P = Library.forall P S; |
63 *} |
63 *} |
64 |
64 |
65 code_generate "op mem" |
65 code_generate ("op mem") |
66 |
66 |
67 code_primconst "insert" |
67 code_primconst "insert" |
68 depending_on ("List.const.member") |
68 depending_on ("List.const.member") |
69 ml {* |
69 ml {* |
70 fun insert x xs = |
70 fun insert x xs = |