[isabelle] adding/deleting transfer rules



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.