1.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy	Mon Jun 21 22:08:01 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy	Sun Jul 18 18:15:27 2021 +0200
     1.3 @@ -6,7 +6,8 @@
     1.4  begin
     1.5  subsection \<open>theorems for Base_Tools\<close>
     1.6  
     1.7 -lemma real_unari_minus:   "- a = (-1) * (a::real)" by auto
     1.8 +lemma real_unari_minus:   "Not (a is_const) ==> - a = (-1) * (a::real)" by auto
     1.9 +(*lemma real_unari_minus:   "- a = (-1) * (a::real)" by auto LOOPS WITH NUMERALS*)
    1.10  (*Semiring_Normalization.comm_ring_1_class.ring_normalization_rules(1)*)
    1.11  
    1.12  (* should be in Rational.thy, but needed for asms in e.g. d2_pqformula1 in PolyEq, RootEq... *)