equal
deleted
inserted
replaced
246 val (thy, {rules = rules_idx, induct, tcs}) = |
246 val (thy, {rules = rules_idx, induct, tcs}) = |
247 tfl_fn strict thy cs (ss delcongs [imp_cong]) |
247 tfl_fn strict thy cs (ss delcongs [imp_cong]) |
248 congs wfs name R eqs; |
248 congs wfs name R eqs; |
249 val rules = map (map #1) (Library.partition_eq Library.eq_snd rules_idx); |
249 val rules = map (map #1) (Library.partition_eq Library.eq_snd rules_idx); |
250 val simp_att = if null tcs then |
250 val simp_att = if null tcs then |
251 [Simplifier.simp_add_global, RecfunCodegen.add] else []; |
251 [Simplifier.simp_add_global, RecfunCodegen.add NONE] else []; |
252 |
252 |
253 val (thy, (simps' :: rules', [induct'])) = |
253 val (thy, (simps' :: rules', [induct'])) = |
254 thy |
254 thy |
255 |> Theory.add_path bname |
255 |> Theory.add_path bname |
256 |> PureThy.add_thmss ((("simps", List.concat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts)) |
256 |> PureThy.add_thmss ((("simps", List.concat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts)) |