1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Thu Sep 16 12:23:57 2021 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Thu Sep 16 17:23:54 2021 +0200
     1.3 @@ -14,10 +14,6 @@
     1.4    (all named eval_*), such that Isac's rewrite engine can handle it.
     1.5  \<close>
     1.6  
     1.7 -subsection \<open>Power re-defined for a specific type\<close>
     1.8 -abbreviation real_powr :: "real \<Rightarrow> real \<Rightarrow> real"  (infixr "\<up>" 80)
     1.9 -where "x \<up> a \<equiv> x powr a"
    1.10 -
    1.11  subsection \<open>consts of functions in pre-conditions and program-expressions\<close>
    1.12  consts
    1.13    lhs             :: "bool => real"           (*of an equality*)
    1.14 @@ -307,7 +303,7 @@
    1.15  (*. evaluate binary, associative, commutative operators: *,+,^ .*)
    1.16  (*("PLUS"    ,(\<^const_name>\<open>plus\<close>        , (**)eval_binop "#add_")),
    1.17    ("TIMES"   ,(\<^const_name>\<open>times\<close>        , (**)eval_binop "#mult_")),
    1.18 -  ("POWER"  ,(\<^const_name>\<open>powr\<close>  , (**)eval_binop "#power_"))*)
    1.19 +  ("POWER"  ,(\<^const_name>\<open>realpow\<close>  , (**)eval_binop "#power_"))*)
    1.20  
    1.21  (* val (thmid,op_,t as(Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2)),thy) =
    1.22         ("xxxxxx",op_,t,thy);