1.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy	Thu Oct 24 14:08:32 2013 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy	Thu Oct 24 15:00:44 2013 +0200
     1.3 @@ -108,9 +108,6 @@
     1.4       (merge_rls "" rateq_erls
     1.5        (append_rls "" e_rls
     1.6  		[])));
     1.7 -
     1.8 -ruleset' := overwritelthy @{theory} (!ruleset',
     1.9 -	     [("RooRatEq_erls",RooRatEq_erls) (*FIXXXME:del with rls.rls'*)]);
    1.10  *}
    1.11  setup {* KEStore_Elems.add_rlss
    1.12    [("RooRatEq_erls", (Context.theory_name @{theory}, RooRatEq_erls))] *}
    1.13 @@ -132,10 +129,6 @@
    1.14        Thm("rootrat_equation_right_2",num_str @{thm rootrat_equation_right_2})
    1.15  		(* [|f is_rootTerm_in bdv|] ==> ( (a =  e/f) = ( a  * f = e ))*)
    1.16        ], scr = Prog ((term_of o the o (parse thy)) "empty_script")}:rls);
    1.17 -
    1.18 -ruleset' := overwritelthy @{theory} (!ruleset',
    1.19 -			[("rootrat_solve",rootrat_solve)
    1.20 -			 ]);
    1.21  *}
    1.22  setup {* KEStore_Elems.add_rlss
    1.23    [("rootrat_solve", (Context.theory_name @{theory}, rootrat_solve))] *}