1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Sun May 02 15:55:37 2021 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Mon May 03 08:49:50 2021 +0200
     1.3 @@ -15,8 +15,8 @@
     1.4  \<close>
     1.5  
     1.6  subsection \<open>Power re-defined for a specific type\<close>
     1.7 -consts
     1.8 -  pow              :: "[real, real] => real"    (infixr "\<up>" 80)
     1.9 +abbreviation real_powr :: "real \<Rightarrow> real \<Rightarrow> real"  (infixr "\<up>" 80)
    1.10 +where "x \<up> a \<equiv> x powr a"
    1.11  
    1.12  subsection \<open>consts of functions in pre-conditions and program-expressions\<close>
    1.13  consts
    1.14 @@ -322,7 +322,7 @@
    1.15  (*. evaluate binary, associative, commutative operators: *,+,^ .*)
    1.16  (*("PLUS"    ,("Groups.plus_class.plus"        , (**)eval_binop "#add_")),
    1.17    ("TIMES"   ,("Groups.times_class.times"        , (**)eval_binop "#mult_")),
    1.18 -  ("POWER"  ,("Prog_Expr.pow"  , (**)eval_binop "#power_"))*)
    1.19 +  ("POWER"  ,("Transcendental.powr"  , (**)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);
    1.23 @@ -547,4 +547,4 @@
    1.24  \<close> ML \<open>
    1.25  \<close>
    1.26  
    1.27 -end
    1.28 \ No newline at end of file
    1.29 +end