9 signature NOMINAL_DT_QUOT = |
9 signature NOMINAL_DT_QUOT = |
10 sig |
10 sig |
11 val define_qtypes: (string list * binding * mixfix) list -> typ list -> term list -> |
11 val define_qtypes: (string list * binding * mixfix) list -> typ list -> term list -> |
12 thm list -> local_theory -> Quotient_Info.quotients list * local_theory |
12 thm list -> local_theory -> Quotient_Info.quotients list * local_theory |
13 |
13 |
14 val define_qconsts: typ list -> (string * term * mixfix) list -> local_theory -> |
14 val define_qconsts: typ list -> (string * term * mixfix * thm) list -> local_theory -> |
15 Quotient_Info.quotconsts list * local_theory |
15 Quotient_Info.quotconsts list * local_theory |
16 |
16 |
17 val define_qperms: typ list -> string list -> (string * sort) list -> |
17 val define_qperms: typ list -> string list -> (string * sort) list -> |
18 (string * term * mixfix) list -> thm list -> local_theory -> local_theory |
18 (string * term * mixfix * thm) list -> thm list -> local_theory -> local_theory |
19 |
19 |
20 val define_qsizes: typ list -> string list -> (string * sort) list -> |
20 val define_qsizes: typ list -> string list -> (string * sort) list -> |
21 (string * term * mixfix) list -> local_theory -> local_theory |
21 (string * term * mixfix * thm) list -> local_theory -> local_theory |
22 |
22 |
23 val lift_thms: typ list -> thm list -> thm list -> Proof.context -> thm list * Proof.context |
23 val lift_thms: typ list -> thm list -> thm list -> Proof.context -> thm list * Proof.context |
24 |
24 |
25 val prove_supports: Proof.context -> thm list -> term list -> thm list |
25 val prove_supports: Proof.context -> thm list -> term list -> thm list |
26 val prove_fsupp: Proof.context -> typ list -> thm -> thm list -> thm list |
26 val prove_fsupp: Proof.context -> typ list -> thm -> thm list -> thm list |