1.1 --- a/src/Tools/isac/IsacKnowledge/LinEq.thy	Wed Aug 25 15:15:01 2010 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,50 +0,0 @@
     1.4 -(*. (c) by Richard Lang, 2003 .*)
     1.5 -(* theory collecting all knowledge for LinearEquations
     1.6 -   created by: rlang 
     1.7 -         date: 02.10
     1.8 -   changed by: rlang
     1.9 -   last change by: rlang
    1.10 -             date: 02.10.20
    1.11 -*)
    1.12 -
    1.13 -(*
    1.14 - use"knowledge/LinEq.ML";
    1.15 - use"LinEq.ML";
    1.16 -
    1.17 - use"ROOT.ML";
    1.18 - cd"knowledge";
    1.19 -
    1.20 -*)
    1.21 -
    1.22 -LinEq = Poly + Equation +
    1.23 -
    1.24 -(*-------------------- consts------------------------------------------------*)
    1.25 -consts
    1.26 -   Solve'_lineq'_equation
    1.27 -             :: "[bool,real, \
    1.28 -		  \ bool list] => bool list"
    1.29 -               ("((Script Solve'_lineq'_equation (_ _ =))// \
    1.30 -                 \ (_))" 9)
    1.31 -
    1.32 -(*-------------------- rules -------------------------------------------------*)
    1.33 -rules
    1.34 -(*-- normalize --*)
    1.35 -  (*WN0509 compare PolyEq.all_left "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)"*)
    1.36 -  all_left
    1.37 -    "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)"
    1.38 -  makex1_x
    1.39 -    "a^^^1  = a"  
    1.40 -  real_assoc_1
    1.41 -   "a+(b+c) = a+b+c"
    1.42 -  real_assoc_2
    1.43 -   "a*(b*c) = a*b*c"
    1.44 -
    1.45 -(*-- solve --*)
    1.46 -  lin_isolate_add1
    1.47 -   "(a + b*bdv = 0) = (b*bdv = (-1)*a)"
    1.48 -  lin_isolate_add2
    1.49 -   "(a +   bdv = 0) = (  bdv = (-1)*a)"
    1.50 -  lin_isolate_div
    1.51 -   "[|Not(b=0)|] ==> (b*bdv = c) = (bdv = c / b)"
    1.52 -end
    1.53 -