1.1 --- a/src/Tools/isac/Knowledge/RootRat.thy	Mon Jul 12 17:21:37 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/RootRat.thy	Tue Jul 13 08:52:35 2021 +0200
     1.3 @@ -20,8 +20,8 @@
     1.4  		      (* w*(z1.0 + z2.0) = w * z1.0 + w * z2.0 *)
     1.5  		     Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),
     1.6  		      (* 1 * z = z *)
     1.7 -		     Rule.Thm ("sym_real_mult_minus1",ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym})),
     1.8 -		       (* "- z1 = -1 * z1"  *)
     1.9 +		      Rule.Thm ("real_mult_minus1_sym", ThmC.numerals_to_Free (@{thm real_mult_minus1_sym})),
    1.10 +	        (*"\<not>(z is_const) ==> - (z::real) = -1 * z"*)
    1.11  		     Rule.Eval ("NthRoot.sqrt", eval_sqrt "#sqrt_")
    1.12  		     ];
    1.13