equal
deleted
inserted
replaced
50 fun is_rateqation_in t v = |
50 fun is_rateqation_in t v = |
51 let |
51 let |
52 fun coeff_in c v = member op = (vars c) v; |
52 fun coeff_in c v = member op = (vars c) v; |
53 fun finddivide (_ $ _ $ _ $ _) v = raise error("is_rateqation_in:") |
53 fun finddivide (_ $ _ $ _ $ _) v = raise error("is_rateqation_in:") |
54 (* at the moment there is no term like this, but ....*) |
54 (* at the moment there is no term like this, but ....*) |
55 | finddivide (t as (Const ("HOL.divide",_) $ _ $ b)) v = coeff_in b v |
55 | finddivide (t as (Const ("Rings.inverse_class.divide",_) $ _ $ b)) v = coeff_in b v |
56 | finddivide (_ $ t1 $ t2) v = (finddivide t1 v) |
56 | finddivide (_ $ t1 $ t2) v = (finddivide t1 v) |
57 orelse (finddivide t2 v) |
57 orelse (finddivide t2 v) |
58 | finddivide (_ $ t1) v = (finddivide t1 v) |
58 | finddivide (_ $ t1) v = (finddivide t1 v) |
59 | finddivide _ _ = false; |
59 | finddivide _ _ = false; |
60 in |
60 in |
92 val rateq_erls = |
92 val rateq_erls = |
93 remove_rls "rateq_erls" (*WN: ein Hack*) |
93 remove_rls "rateq_erls" (*WN: ein Hack*) |
94 (merge_rls "is_ratequation_in" calculate_Rational |
94 (merge_rls "is_ratequation_in" calculate_Rational |
95 (append_rls "is_ratequation_in" |
95 (append_rls "is_ratequation_in" |
96 Poly_erls |
96 Poly_erls |
97 [(*Calc ("HOL.divide", eval_cancel "#divide_e"),*) |
97 [(*Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),*) |
98 Calc ("RatEq.is'_ratequation'_in", |
98 Calc ("RatEq.is'_ratequation'_in", |
99 eval_is_ratequation_in "") |
99 eval_is_ratequation_in "") |
100 |
100 |
101 ])) |
101 ])) |
102 [Thm ("and_commute",num_str @{thm and_commute}), (*WN: ein Hack*) |
102 [Thm ("and_commute",num_str @{thm and_commute}), (*WN: ein Hack*) |
110 val RatEq_crls = |
110 val RatEq_crls = |
111 remove_rls "RatEq_crls" (*WN: ein Hack*) |
111 remove_rls "RatEq_crls" (*WN: ein Hack*) |
112 (merge_rls "is_ratequation_in" calculate_Rational |
112 (merge_rls "is_ratequation_in" calculate_Rational |
113 (append_rls "is_ratequation_in" |
113 (append_rls "is_ratequation_in" |
114 Poly_erls |
114 Poly_erls |
115 [(*Calc ("HOL.divide", eval_cancel "#divide_e"),*) |
115 [(*Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"),*) |
116 Calc ("RatEq.is'_ratequation'_in", |
116 Calc ("RatEq.is'_ratequation'_in", |
117 eval_is_ratequation_in "") |
117 eval_is_ratequation_in "") |
118 ])) |
118 ])) |
119 [Thm ("and_commute",num_str @{thm and_commute}), (*WN: ein Hack*) |
119 [Thm ("and_commute",num_str @{thm and_commute}), (*WN: ein Hack*) |
120 Thm ("or_commute",num_str @{thm or_commute}) (*WN: ein Hack*) |
120 Thm ("or_commute",num_str @{thm or_commute}) (*WN: ein Hack*) |