1.1 --- a/src/Tools/isac/ProgLang/Calculate.thy	Mon Jul 19 18:29:46 2021 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/Calculate.thy	Mon Jul 19 18:39:02 2021 +0200
     1.3 @@ -13,8 +13,7 @@
     1.4    Since that time numeral calculations are done by ML functions, all named eval_ 
     1.5    and integrated into rewriting. eval_binop below is not bound to a specific constant
     1.6    (like in Prog_Expr.thy), rather calculates results of Isabelle's binary operations + - * / ^.
     1.7 -  Nowadays the code in Calculate.thy and evaluate.sml should be replaced by native Isabelle
     1.8 -  code.
     1.9 +
    1.10    A specialty are the ad-hoc theorems for numeral calculations created in order to provide
    1.11    the rewrite engine with theorems as done in general.
    1.12  \<close>