1.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Mon May 03 08:49:50 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Mon May 03 09:36:47 2021 +0200
     1.3 @@ -639,7 +639,7 @@
     1.4  
     1.5  	       (*----- distribute none-atoms -----*)
     1.6  	       Rule.Thm ("realpow_def_atom",ThmC.numerals_to_Free @{thm realpow_def_atom}),
     1.7 -	       (*"[| 1 < n; not(r is_atom) |]==>r  \<up>  n = r * r  \<up>  (n + -1)"*)
     1.8 +	       (*"[| 1 < n; ~ (r is_atom) |]==>r  \<up>  n = r * r  \<up>  (n + -1)"*)
     1.9  	       Rule.Thm ("realpow_eq_oneI",ThmC.numerals_to_Free @{thm realpow_eq_oneI}),
    1.10  	       (*"1  \<up>  n = 1"*)
    1.11  	       Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_")