1.1 --- a/src/Tools/isac/Knowledge/RootRat.thy	Tue Jul 27 11:21:14 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/RootRat.thy	Tue Jul 27 12:32:43 2021 +0200
     1.3 @@ -15,15 +15,11 @@
     1.4  
     1.5  (*.calculate numeral groundterms.*)
     1.6  val calculate_RootRat = 
     1.7 -  Rule_Set.append_rules "calculate_RootRat" calculate_Rational
     1.8 -	    [\<^rule_thm>\<open>distrib_left\<close>,
     1.9 -		      (* w*(z1.0 + z2.0) = w * z1.0 + w * z2.0 *)
    1.10 -		     \<^rule_thm>\<open>mult_1_left\<close>,
    1.11 -		      (* 1 * z = z *)
    1.12 -		      Rule.Thm ("real_mult_minus1_sym",  (@{thm real_mult_minus1_sym})),
    1.13 -	        (*"\<not>(z is_const) ==> - (z::real) = -1 * z"*)
    1.14 -		     Rule.Eval ("NthRoot.sqrt", eval_sqrt "#sqrt_")
    1.15 -		     ];
    1.16 +  Rule_Set.append_rules "calculate_RootRat" calculate_Rational [
    1.17 +    \<^rule_thm>\<open>distrib_left\<close> (* w*(z1.0 + z2.0) = w * z1.0 + w * z2.0 *),
    1.18 +		\<^rule_thm>\<open>mult_1_left\<close> (* 1 * z = z *),
    1.19 +    \<^rule_thm>\<open>real_mult_minus1_sym\<close> (*"\<not>(z is_const) ==> - (z::real) = -1 * z"*),
    1.20 +		\<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_")];
    1.21  
    1.22  val prep_rls' = Auto_Prog.prep_rls @{theory};
    1.23  \<close>