equal
deleted
inserted
replaced
75 else SOME ((UnparseC.term p) ^ " = False", |
75 else SOME ((UnparseC.term p) ^ " = False", |
76 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))) |
76 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))) |
77 | eval_occur_exactly_in _ _ _ _ = NONE; |
77 | eval_occur_exactly_in _ _ _ _ = NONE; |
78 \<close> |
78 \<close> |
79 setup \<open>KEStore_Elems.add_calcs |
79 setup \<open>KEStore_Elems.add_calcs |
80 [("occur_exactly_in", |
80 [("occur_exactly_in", (\<^const_name>\<open>occur_exactly_in\<close>, eval_occur_exactly_in "#eval_occur_exactly_in_"))]\<close> |
81 ("EqSystem.occur_exactly_in", |
|
82 eval_occur_exactly_in "#eval_occur_exactly_in_"))]\<close> |
|
83 ML \<open> |
81 ML \<open> |
84 (** rewrite order 'ord_simplify_System' **) |
82 (** rewrite order 'ord_simplify_System' **) |
85 |
83 |
86 (* order wrt. several linear (i.e. without exponents) variables "c", "c_2",.. |
84 (* order wrt. several linear (i.e. without exponents) variables "c", "c_2",.. |
87 which leaves the monomials containing c, c_2,... at the end of an Integral |
85 which leaves the monomials containing c, c_2,... at the end of an Integral |