Re: [isabelle] adding/deleting transfer rules



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.