equal
deleted
inserted
replaced
587 Where: |
587 Where: |
588 "(matches ( v_v = 0) e_e) | (matches ( ?b*v_v = 0) e_e) | |
588 "(matches ( v_v = 0) e_e) | (matches ( ?b*v_v = 0) e_e) | |
589 (matches (?a+v_v = 0) e_e) | (matches (?a+?b*v_v = 0) e_e)" |
589 (matches (?a+v_v = 0) e_e) | (matches (?a+?b*v_v = 0) e_e)" |
590 Find: "solutions v_v'i'" |
590 Find: "solutions v_v'i'" |
591 |
591 |
|
592 setup \<open>KEStore_Elems.add_rew_ord [ |
|
593 ("termlessI", termlessI), |
|
594 ("ord_make_polytest", ord_make_polytest false \<^theory>)]\<close> |
|
595 |
592 ML \<open> |
596 ML \<open> |
593 Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord', |
|
594 [("termlessI", termlessI), |
|
595 ("ord_make_polytest", ord_make_polytest false \<^theory>) |
|
596 ]); |
|
597 |
|
598 val make_polytest = |
597 val make_polytest = |
599 Rule_Def.Repeat{id = "make_polytest", preconds = []:term list, |
598 Rule_Def.Repeat{id = "make_polytest", preconds = []:term list, |
600 rew_ord = ("ord_make_polytest", ord_make_polytest false @{theory "Poly"}), |
599 rew_ord = ("ord_make_polytest", ord_make_polytest false @{theory "Poly"}), |
601 erls = testerls, srls = Rule_Set.Empty, |
600 erls = testerls, srls = Rule_Set.Empty, |
602 calc = [ |
601 calc = [ |