1.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Sat Jun 12 14:27:03 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Sat Jun 12 14:29:10 2021 +0200
     1.3 @@ -691,8 +691,7 @@
     1.4  	       (*Rule.Thm ("right_minus",ThmC.numerals_to_Free @{thm right_minus}),
     1.5  	       "?z + - ?z = 0"*)
     1.6  
     1.7 -	       Rule.Thm ("sym_real_mult_2",
     1.8 -                     ThmC.numerals_to_Free (@{thm real_mult_2} RS @{thm sym})),	
     1.9 +	       \<^rule_thm_sym>\<open>real_mult_2\<close>,	
    1.10  	       (*"z1 + z1 = 2 * z1"*)
    1.11  	       Rule.Thm ("real_mult_2_assoc",ThmC.numerals_to_Free @{thm real_mult_2_assoc}),
    1.12  	       (*"z1 + (z1 + k) = 2 * z1 + k"*)