1.1 --- a/src/Tools/isac/IsacKnowledge/RootRatEq.thy	Wed Aug 25 15:15:01 2010 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,48 +0,0 @@
     1.4 -(*.c) by Richard Lang, 2003 .*)
     1.5 -(* collecting all knowledge for Root and Rational Equations
     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.11.04
    1.11 -*)
    1.12 -
    1.13 -(* use"knowledge/RootRatEq.ML";
    1.14 -   use"RootRatEq.ML";
    1.15 -
    1.16 -   use"ROOT.ML";
    1.17 -   cd"knowledge";
    1.18 -
    1.19 -   remove_thy"RootRatEq";
    1.20 -   use_thy"Isac";
    1.21 -   *)
    1.22 -
    1.23 -RootRatEq = RootEq + RatEq + RootRat + 
    1.24 -
    1.25 -(*-------------------- consts-----------------------------------------------*)
    1.26 -consts
    1.27 -
    1.28 -  is'_rootRatAddTerm'_in :: [real, real] => bool ("_ is'_rootRatAddTerm'_in _") (*RL DA*)
    1.29 -
    1.30 -(*---------scripts--------------------------*)
    1.31 -  Elim'_rootrat'_equation
    1.32 -             :: "[bool,real, \
    1.33 -		  \ bool list] => bool list"
    1.34 -               ("((Script Elim'_rootrat'_equation (_ _ =))// \
    1.35 -                 \ (_))" 9)
    1.36 - (*-------------------- rules------------------------------------------------*)
    1.37 -rules
    1.38 -
    1.39 -  (* eliminate ratRootTerm *)
    1.40 -  rootrat_equation_left_1
    1.41 -   "[|c is_rootTerm_in bdv|] ==> ( (a + b/c = d) = ( b = (d - a) * c ))"
    1.42 -  rootrat_equation_left_2
    1.43 -   "[|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c ))"
    1.44 -  rootrat_equation_right_2
    1.45 -   "[|f is_rootTerm_in bdv|] ==> ( (a = d + e/f) = ( (a - d) * f = e ))"
    1.46 -  rootrat_equation_right_1
    1.47 -   "[|f is_rootTerm_in bdv|] ==> ( (a = e/f) = ( a * f = e ))"
    1.48 -
    1.49 -
    1.50 -
    1.51 -end