9 val cert_def: Proof.context -> term -> (string * typ) * term |
9 val cert_def: Proof.context -> term -> (string * typ) * term |
10 val abs_def: term -> (string * typ) * term |
10 val abs_def: term -> (string * typ) * term |
11 val mk_def: Proof.context -> (string * term) list -> term list |
11 val mk_def: Proof.context -> (string * term) list -> term list |
12 val expand: cterm list -> thm -> thm |
12 val expand: cterm list -> thm -> thm |
13 val def_export: Assumption.export |
13 val def_export: Assumption.export |
14 val add_defs: ((Binding.T * mixfix) * ((Binding.T * attribute list) * term)) list -> |
14 val add_defs: ((binding * mixfix) * ((binding * attribute list) * term)) list -> |
15 Proof.context -> (term * (string * thm)) list * Proof.context |
15 Proof.context -> (term * (string * thm)) list * Proof.context |
16 val add_def: (Binding.T * mixfix) * term -> Proof.context -> (term * thm) * Proof.context |
16 val add_def: (binding * mixfix) * term -> Proof.context -> (term * thm) * Proof.context |
17 val fixed_abbrev: (Binding.T * mixfix) * term -> Proof.context -> |
17 val fixed_abbrev: (binding * mixfix) * term -> Proof.context -> |
18 (term * term) * Proof.context |
18 (term * term) * Proof.context |
19 val export: Proof.context -> Proof.context -> thm -> thm list * thm |
19 val export: Proof.context -> Proof.context -> thm -> thm list * thm |
20 val export_cterm: Proof.context -> Proof.context -> cterm -> cterm * thm |
20 val export_cterm: Proof.context -> Proof.context -> cterm -> cterm * thm |
21 val trans_terms: Proof.context -> thm list -> thm |
21 val trans_terms: Proof.context -> thm list -> thm |
22 val trans_props: Proof.context -> thm list -> thm |
22 val trans_props: Proof.context -> thm list -> thm |