Am 02.12.2011 um 15:52 schrieb Lukas Bulwahn:
>>
> It is best practice to make your data storage local, i.e., to a Generic_Data
> functor.
> Then update the generic data storage with Local_Theory.declaration.
>
> Looking in the sources for the usage of Local_Theory.declaration should give
> you a rough pattern, how to employ this function.
>
>> The second is a rather simple ML question:
>> - Is it possible to conveniently update single fields in a record as in
>> OCaml?
>> E.g., val r1 = {a = 5, b = "foo", c = ..} and many fields
>> val r2 = '' r1 where only b is changed to "bar" ''
>> (in OCaml: val r2 = {r1 with b = "bar"})
>
> To my knowledge, there is no convenient update functions for record in ML
> provided automatically.
> Therefore, many developers just define the ones of interest with some
> boiler-plate code.
thanks for the pointers, now I can continue.
Best regards,
René
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
