Re: [isabelle] adding/deleting transfer rules



Thank you, Ondřej. Your suggestion worked.


On 6 August 2014 16:29, Ondřej Kunčar <kuncar at in.tum.de> wrote:

> Hi Daniel,
> the default entry points are two attributes Transfer.transfer_add and
> Transfer.transfer_del. They do internally some preprocessing and call
> Transfer.transfer_raw_add (or Transfer.transfer_raw_del) at the end.
>
> You shouldn't use Transfer.transfer_raw_add and Transfer.transfer_raw_del
> unless you really know what you are doing.
>
> Ad using the attributes:
> If you are in a local_theory context, use Local_Theory.note. E.g.,
> Local_Theory.note ((Binding.empty, [transfer_attr]), [transfer_rule])
> where transfer_attr = Attrib.internal (K Transfer.transfer_add).
>
> If you are in a global context, you can use Thm.attribute_declaration.
> (e.g., Thm.attribute_declaration Transfer.transfer_add transfer_rule).
>
> Ondrej
>
>
> On 08/06/2014 05:10 PM, Daniel Raggi wrote:
>
>> How do I add or delete transfer rules at the ML level? I have found
>> functions Transfer.transfer_raw_add and Transfer.transfer_raw_del, but
>> I've
>> realised that there must have been some renaming of the theorems when they
>> where added to the database of transfer rules, because the name I gave to
>> the theorems when declaring them doesn't work to add or remove them. So
>> what names can I use to access them?
>>
>> I'm thinking that it's not just the name, but that something else has to
>> be
>> done to the transfer rules to be usable by the transfer engine (adding
>> Transfer.Rel to rules that relate two constants?). This probably means
>> that
>> if I want to add the rules at the ML level I also have to do that first.
>> Am
>> I on the right track?
>>
>> Thanks.
>>
>> Daniel
>>
>>
>
>



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.