equal
deleted
inserted
replaced
845 val transfer_domain_attribute = |
845 val transfer_domain_attribute = |
846 Attrib.add_del transfer_domain_add transfer_domain_del |
846 Attrib.add_del transfer_domain_add transfer_domain_del |
847 |
847 |
848 (* Attributes for transferred rules *) |
848 (* Attributes for transferred rules *) |
849 |
849 |
850 fun transferred_attribute thms = Thm.rule_attribute |
850 fun transferred_attribute thms = |
851 (fn context => transferred (Context.proof_of context) thms) |
851 Thm.rule_attribute thms (fn context => transferred (Context.proof_of context) thms) |
852 |
852 |
853 fun untransferred_attribute thms = Thm.rule_attribute |
853 fun untransferred_attribute thms = |
854 (fn context => untransferred (Context.proof_of context) thms) |
854 Thm.rule_attribute thms (fn context => untransferred (Context.proof_of context) thms) |
855 |
855 |
856 val transferred_attribute_parser = |
856 val transferred_attribute_parser = |
857 Attrib.thms >> transferred_attribute |
857 Attrib.thms >> transferred_attribute |
858 |
858 |
859 val untransferred_attribute_parser = |
859 val untransferred_attribute_parser = |