equal
deleted
inserted
replaced
13 type pcr = {pcrel_def: thm, pcr_cr_eq: thm} |
13 type pcr = {pcrel_def: thm, pcr_cr_eq: thm} |
14 type quotient = {quot_thm: thm, pcr_info: pcr option} |
14 type quotient = {quot_thm: thm, pcr_info: pcr option} |
15 val transform_quotient: morphism -> quotient -> quotient |
15 val transform_quotient: morphism -> quotient -> quotient |
16 val lookup_quotients: Proof.context -> string -> quotient option |
16 val lookup_quotients: Proof.context -> string -> quotient option |
17 val update_quotients: string -> quotient -> Context.generic -> Context.generic |
17 val update_quotients: string -> quotient -> Context.generic -> Context.generic |
|
18 val delete_quotients: thm -> Context.generic -> Context.generic |
18 val print_quotients: Proof.context -> unit |
19 val print_quotients: Proof.context -> unit |
19 |
20 |
20 val get_invariant_commute_rules: Proof.context -> thm list |
21 val get_invariant_commute_rules: Proof.context -> thm list |
21 |
22 |
22 val get_reflexivity_rules: Proof.context -> thm list |
23 val get_reflexivity_rules: Proof.context -> thm list |