equal
deleted
inserted
replaced
1812 fun lhs_of_equation (Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t $ _) = t |
1812 fun lhs_of_equation (Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t $ _) = t |
1813 | lhs_of_equation (\<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t $ _)) = t; |
1813 | lhs_of_equation (\<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t $ _)) = t; |
1814 |
1814 |
1815 fun add_spec_rule rule = |
1815 fun add_spec_rule rule = |
1816 let val head = head_of (lhs_of_equation (Thm.prop_of rule)) |
1816 let val head = head_of (lhs_of_equation (Thm.prop_of rule)) |
1817 in Spec_Rules.add_global "" Spec_Rules.equational [head] [rule] end; |
1817 in Spec_Rules.add_global Binding.empty Spec_Rules.equational [head] [rule] end; |
1818 |
1818 |
1819 (* definition *) |
1819 (* definition *) |
1820 |
1820 |
1821 fun definition overloaded (alphas, binding) parent (parents: parent_info list) raw_fields thy0 = |
1821 fun definition overloaded (alphas, binding) parent (parents: parent_info list) raw_fields thy0 = |
1822 let |
1822 let |