equal
deleted
inserted
replaced
7 signature TRANSFER = |
7 signature TRANSFER = |
8 sig |
8 sig |
9 val prep_conv: conv |
9 val prep_conv: conv |
10 val get_relator_eq: Proof.context -> thm list |
10 val get_relator_eq: Proof.context -> thm list |
11 val get_sym_relator_eq: Proof.context -> thm list |
11 val get_sym_relator_eq: Proof.context -> thm list |
|
12 val get_relator_eq_raw: Proof.context -> thm list |
12 val get_transfer_raw: Proof.context -> thm list |
13 val get_transfer_raw: Proof.context -> thm list |
13 val transfer_add: attribute |
14 val transfer_add: attribute |
14 val transfer_del: attribute |
15 val transfer_del: attribute |
15 val transfer_rule_of_term: Proof.context -> term -> thm |
16 val transfer_rule_of_term: Proof.context -> term -> thm |
16 val transfer_tac: bool -> Proof.context -> int -> tactic |
17 val transfer_tac: bool -> Proof.context -> int -> tactic |