changeset 51374 | 84d01fd733cf |
parent 51314 | eac4bb5adbf9 |
child 51437 | 8739f8abbecb |
--- a/src/HOL/Tools/transfer.ML Fri Mar 08 11:28:20 2013 +0100 +++ b/src/HOL/Tools/transfer.ML Fri Mar 08 13:14:23 2013 +0100 @@ -9,6 +9,7 @@ val prep_conv: conv val get_relator_eq: Proof.context -> thm list val get_sym_relator_eq: Proof.context -> thm list + val get_transfer_raw: Proof.context -> thm list val transfer_add: attribute val transfer_del: attribute val transfer_rule_of_term: Proof.context -> term -> thm