equal
deleted
inserted
replaced
19 val dest_quotients: Proof.context -> quotients list |
19 val dest_quotients: Proof.context -> quotients list |
20 val print_quotients: Proof.context -> unit |
20 val print_quotients: Proof.context -> unit |
21 |
21 |
22 val get_invariant_commute_rules: Proof.context -> thm list |
22 val get_invariant_commute_rules: Proof.context -> thm list |
23 |
23 |
24 val get_reflp_preserve_rules: Proof.context -> thm list |
24 val get_reflexivity_rules: Proof.context -> thm list |
25 val add_reflp_preserve_rule_attribute: attribute |
25 val add_reflexivity_rule_attribute: attribute |
26 val add_reflp_preserve_rule_attrib: Attrib.src |
26 val add_reflexivity_rule_attrib: Attrib.src |
27 |
27 |
28 val setup: theory -> theory |
28 val setup: theory -> theory |
29 end; |
29 end; |
30 |
30 |
31 structure Lifting_Info: LIFTING_INFO = |
31 structure Lifting_Info: LIFTING_INFO = |
181 |
181 |
182 fun get_invariant_commute_rules ctxt = map safe_mk_meta_eq (Invariant_Commute.get ctxt) |
182 fun get_invariant_commute_rules ctxt = map safe_mk_meta_eq (Invariant_Commute.get ctxt) |
183 |
183 |
184 structure Reflp_Preserve = Named_Thms |
184 structure Reflp_Preserve = Named_Thms |
185 ( |
185 ( |
186 val name = @{binding reflp_preserve} |
186 val name = @{binding reflexivity_rule} |
187 val description = "theorems that a relator preserves a reflexivity property" |
187 val description = "theorems that a relator preserves a reflexivity property" |
188 ) |
188 ) |
189 |
189 |
190 val get_reflp_preserve_rules = Reflp_Preserve.get |
190 val get_reflexivity_rules = Reflp_Preserve.get |
191 val add_reflp_preserve_rule_attribute = Reflp_Preserve.add |
191 val add_reflexivity_rule_attribute = Reflp_Preserve.add |
192 val add_reflp_preserve_rule_attrib = Attrib.internal (K add_reflp_preserve_rule_attribute) |
192 val add_reflexivity_rule_attrib = Attrib.internal (K add_reflexivity_rule_attribute) |
193 |
193 |
194 (* theory setup *) |
194 (* theory setup *) |
195 |
195 |
196 val setup = |
196 val setup = |
197 quot_map_attribute_setup |
197 quot_map_attribute_setup |