1.1 --- a/src/Tools/isac/Knowledge/RootRat.thy	Thu Mar 15 10:17:44 2018 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/RootRat.thy	Thu Mar 15 12:42:04 2018 +0100
     1.3 @@ -9,20 +9,20 @@
     1.4  val thy = @{theory};
     1.5  
     1.6  val rootrat_erls = 
     1.7 -  merge_rls "rootrat_erls" Root_erls
     1.8 -    (merge_rls "" rational_erls
     1.9 -      (append_rls "" e_rls []));
    1.10 +  Celem.merge_rls "rootrat_erls" Root_erls
    1.11 +    (Celem.merge_rls "" rational_erls
    1.12 +      (Celem.append_rls "" Celem.e_rls []));
    1.13  
    1.14  (*.calculate numeral groundterms.*)
    1.15  val calculate_RootRat = 
    1.16 -  append_rls "calculate_RootRat" calculate_Rational
    1.17 -	    [Thm ("distrib_left",TermC.num_str @{thm distrib_left}),
    1.18 +  Celem.append_rls "calculate_RootRat" calculate_Rational
    1.19 +	    [Celem.Thm ("distrib_left",TermC.num_str @{thm distrib_left}),
    1.20  		      (* w*(z1.0 + z2.0) = w * z1.0 + w * z2.0 *)
    1.21 -		     Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),
    1.22 +		     Celem.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),
    1.23  		      (* 1 * z = z *)
    1.24 -		     Thm ("sym_real_mult_minus1",TermC.num_str (@{thm real_mult_minus1} RS @{thm sym})),
    1.25 +		     Celem.Thm ("sym_real_mult_minus1",TermC.num_str (@{thm real_mult_minus1} RS @{thm sym})),
    1.26  		       (* "- z1 = -1 * z1"  *)
    1.27 -		     Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_")
    1.28 +		     Celem.Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_")
    1.29  		     ];
    1.30  
    1.31  val prep_rls' = LTool.prep_rls @{theory};