1 (*. (c) by Richard Lang, 2003 .*)
2 (* theory collecting all knowledge for LinearEquations
11 use"knowledge/LinEq.ML";
19 LinEq = Poly + Equation +
21 (*-------------------- consts------------------------------------------------*)
23 Solve'_lineq'_equation
25 \ bool list] => bool list"
26 ("((Script Solve'_lineq'_equation (_ _ =))// \
29 (*-------------------- rules -------------------------------------------------*)
32 (*WN0509 compare PolyEq.all_left "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)"*)
34 "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)"
44 "(a + b*bdv = 0) = (b*bdv = (-1)*a)"
46 "(a + bdv = 0) = ( bdv = (-1)*a)"
48 "[|Not(b=0)|] ==> (b*bdv = c) = (bdv = c / b)"