1.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy	Tue Sep 14 12:12:42 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy	Tue Sep 14 15:46:56 2010 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4     (c) by Richard Lang, 2003
     1.5  *)
     1.6  
     1.7 -theory RootRatEq imports RootEq RatEq RootRat begin 
     1.8 +theory RootRatEq imports LinEq RootEq RatEq RootRat begin 
     1.9  
    1.10  consts
    1.11  
    1.12 @@ -144,7 +144,7 @@
    1.13    [("#Given" ,["equality e_e","solveFor v_v"]),
    1.14     ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) )| " ^
    1.15  	       "( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"]),
    1.16 -   ("#Find"  ,["solutions v_i'''"])
    1.17 +   ("#Find"  ,["solutions v'i'"])
    1.18     ],
    1.19    RootRatEq_prls, SOME "solve (e_e::bool, v_v)",
    1.20    [["RootRatEq","elim_rootrat_equation"]]));
    1.21 @@ -164,7 +164,7 @@
    1.22     [("#Given" ,["equality e_e","solveFor v_v"]),
    1.23      ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) ) | " ^
    1.24  	       "( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"]),
    1.25 -    ("#Find"  ,["solutions v_i'''"])
    1.26 +    ("#Find"  ,["solutions v'i'"])
    1.27     ],
    1.28     {rew_ord'="termlessI",
    1.29      rls'=RooRatEq_erls,