583 |
583 |
584 *} |
584 *} |
585 ML {* |
585 ML {* |
586 (** methods **) |
586 (** methods **) |
587 store_met |
587 store_met |
588 (prep_met (Thy_Info.get_theory "Diff") "met_test" [] e_metID |
588 (prep_met @{theory "Diff"} "met_test" [] e_metID |
589 (["Test"], |
589 (["Test"], |
590 [], |
590 [], |
591 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls, |
591 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls, |
592 crls=Atools_erls, errpats = [], nrls = e_rls}, "empty_script")); |
592 crls=Atools_erls, errpats = [], nrls = e_rls}, "empty_script")); |
593 *} |
593 *} |
626 , ---------27.4.02*) |
626 , ---------27.4.02*) |
627 ); |
627 ); |
628 |
628 |
629 *} |
629 *} |
630 ML {* |
630 ML {* |
631 |
|
632 ruleset' := overwritelthy @{theory} (!ruleset', |
631 ruleset' := overwritelthy @{theory} (!ruleset', |
633 [("norm_equation", prep_rls norm_equation), |
632 [("norm_equation", prep_rls norm_equation), |
634 ("ac_plus_times", prep_rls ac_plus_times), |
633 ("ac_plus_times", prep_rls ac_plus_times), |
635 ("rearrange_assoc", prep_rls rearrange_assoc) |
634 ("rearrange_assoc", prep_rls rearrange_assoc) |
636 ]); |
635 ]); |
1318 " t_t)"; |
1317 " t_t)"; |
1319 -----------------------------------------------------*) |
1318 -----------------------------------------------------*) |
1320 |
1319 |
1321 val make_polytest = |
1320 val make_polytest = |
1322 Rls{id = "make_polytest", preconds = []:term list, |
1321 Rls{id = "make_polytest", preconds = []:term list, |
1323 rew_ord = ("ord_make_polytest", ord_make_polytest false (Thy_Info.get_theory "Poly")), |
1322 rew_ord = ("ord_make_polytest", ord_make_polytest false @{theory "Poly"}), |
1324 erls = testerls, srls = Erls, |
1323 erls = testerls, srls = Erls, |
1325 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")), |
1324 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")), |
1326 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")), |
1325 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")), |
1327 ("POWER", ("Atools.pow", eval_binop "#power_")) |
1326 ("POWER", ("Atools.pow", eval_binop "#power_")) |
1328 ], errpatts = [], |
1327 ], errpatts = [], |