equal
deleted
inserted
replaced
189 val (eqn_thms', thy2) = |
189 val (eqn_thms', thy2) = |
190 thy1 |
190 thy1 |
191 |> PureThy.add_thms ((eqn_names ~~ eqn_thms) ~~ eqn_atts); |
191 |> PureThy.add_thms ((eqn_names ~~ eqn_thms) ~~ eqn_atts); |
192 val (_, thy3) = |
192 val (_, thy3) = |
193 thy2 |
193 thy2 |
194 |> PureThy.add_thmss [(("simps", eqn_thms'), [Simplifier.simp_add_global])] |
194 |> PureThy.add_thmss [(("simps", eqn_thms'), [Attrib.theory Simplifier.simp_add])] |
195 ||> Theory.parent_path; |
195 ||> Theory.parent_path; |
196 in (thy3, eqn_thms') end; |
196 in (thy3, eqn_thms') end; |
197 |
197 |
198 fun add_primrec args thy = |
198 fun add_primrec args thy = |
199 add_primrec_i (map (fn ((name, s), srcs) => |
199 add_primrec_i (map (fn ((name, s), srcs) => |