1.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy	Tue Aug 17 22:50:20 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy	Wed Aug 18 11:35:24 2021 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  begin
     1.5  subsection \<open>theorems for Base_Tools\<close>
     1.6  
     1.7 -lemma real_unari_minus:   "Not (a is_const) ==> - a = (-1) * (a::real)" by auto
     1.8 +lemma real_unari_minus:   "Not (a is_num) ==> - 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