366 ("dist_les", dist_les), |
366 ("dist_les", dist_les), |
367 ("dist_eqs", dist_eqs), |
367 ("dist_eqs", dist_eqs), |
368 ("inverts" , inverts ), |
368 ("inverts" , inverts ), |
369 ("injects" , injects ), |
369 ("injects" , injects ), |
370 ("copy_rews", copy_rews)]))) |
370 ("copy_rews", copy_rews)]))) |
371 |> (snd o PureThy.add_thmss [(("match_rews", mat_rews), [Simplifier.simp_add_global])]) |
371 |> (snd o PureThy.add_thmss [(("match_rews", mat_rews), [Attrib.theory Simplifier.simp_add])]) |
372 |> Theory.parent_path |> rpair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @ |
372 |> Theory.parent_path |> rpair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @ |
373 pat_rews @ dist_les @ dist_eqs @ copy_rews) |
373 pat_rews @ dist_les @ dist_eqs @ copy_rews) |
374 end; (* let *) |
374 end; (* let *) |
375 |
375 |
376 fun comp_theorems (comp_dnam, eqs: eq list) thy = |
376 fun comp_theorems (comp_dnam, eqs: eq list) thy = |