equal
deleted
inserted
replaced
160 * Library: added theory Coinductive_List of potentially infinite lists as |
160 * Library: added theory Coinductive_List of potentially infinite lists as |
161 greatest fixed-point. |
161 greatest fixed-point. |
162 |
162 |
163 |
163 |
164 *** ML *** |
164 *** ML *** |
|
165 |
|
166 * Pure: functions of signature "... -> theory -> theory * ..." have been reoriented |
|
167 to "... -> theory -> ... * theory" in order to allow natural usage in combination |
|
168 with the ||>, ||>>, |-> and fold_map combinators. |
|
169 |
|
170 * Library: new module Pure/General/name_mangler providing a functor for generic |
|
171 name mangling (bijective mapping from any expression values to strings). |
|
172 |
|
173 * SML systems: added |
|
174 print: 'a -> 'a |
|
175 to smlnj. PolyML provides such a function which as a side effect prints out |
|
176 a string representation of its argument. By adding print to smlnj, it is possible |
|
177 to use "print" for debugging purpose without breaking smlnj compatibility. |
|
178 |
|
179 * Library: functions map2 and fold2 with curried syntax for simultanous |
|
180 mapping and folding: |
|
181 val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list |
|
182 val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c |
165 |
183 |
166 * Library: new module Pure/General/rat.ML implementing rational numbers, |
184 * Library: new module Pure/General/rat.ML implementing rational numbers, |
167 replacing the former functions in the Isabelle library. |
185 replacing the former functions in the Isabelle library. |
168 |
186 |
169 * Library: indexed lists - some functions in the Isabelle library |
187 * Library: indexed lists - some functions in the Isabelle library |