diff -r 638d02a9a96a -r e6e7a9b9ced7 src/Tools/isac/Knowledge/Base_Tools.thy
--- a/src/Tools/isac/Knowledge/Base_Tools.thy	Tue Jun 01 15:41:23 2021 +0200
+++ b/src/Tools/isac/Knowledge/Base_Tools.thy	Sat Jul 03 16:21:07 2021 +0200
@@ -6,7 +6,8 @@
 begin
 subsection \<open>theorems for Base_Tools\<close>
 
-lemma real_unari_minus:   "- a = (-1) * (a::real)" by auto
+lemma real_unari_minus:   "Not (a is_const) ==> - a = (-1) * (a::real)" by auto
+(*lemma real_unari_minus:   "- a = (-1) * (a::real)" by auto LOOPS WITH NUMERALS*)
 (*Semiring_Normalization.comm_ring_1_class.ring_normalization_rules(1)*)
 
 (* should be in Rational.thy, but needed for asms in e.g. d2_pqformula1 in PolyEq, RootEq... *)