equal
deleted
inserted
replaced
48 (*-------------------------functions-----------------------*) |
48 (*-------------------------functions-----------------------*) |
49 (* is_rateqation_in becomes true, if a bdv is in the denominator of a fraction*) |
49 (* is_rateqation_in becomes true, if a bdv is in the denominator of a fraction*) |
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 = 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 ("Rings.inverse_class.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) |