[isabelle-dev] Two simple beginners question

[René Thiemann]

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é