diff -r 5b1cd0f93d8b -r 98ee674d18d3 src/Tools/isac/Knowledge/Rational.thy
--- a/src/Tools/isac/Knowledge/Rational.thy	Sun May 02 15:55:37 2021 +0200
+++ b/src/Tools/isac/Knowledge/Rational.thy	Mon May 03 08:49:50 2021 +0200
@@ -25,7 +25,7 @@
   | is_ratpolyexp (Const ("Groups.plus_class.plus",_) $ Free _ $ Free _) = true
   | is_ratpolyexp (Const ("Groups.minus_class.minus",_) $ Free _ $ Free _) = true
   | is_ratpolyexp (Const ("Groups.times_class.times",_) $ Free _ $ Free _) = true
-  | is_ratpolyexp (Const ("Prog_Expr.pow",_) $ Free _ $ Free _) = true
+  | is_ratpolyexp (Const ("Transcendental.powr",_) $ Free _ $ Free _) = true
   | is_ratpolyexp (Const ("Rings.divide_class.divide",_) $ Free _ $ Free _) = true
   | is_ratpolyexp (Const ("Groups.plus_class.plus",_) $ t1 $ t2) = 
                ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
@@ -33,7 +33,7 @@
                ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
   | is_ratpolyexp (Const ("Groups.times_class.times",_) $ t1 $ t2) = 
                ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
-  | is_ratpolyexp (Const ("Prog_Expr.pow",_) $ t1 $ t2) = 
+  | is_ratpolyexp (Const ("Transcendental.powr",_) $ t1 $ t2) = 
                ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
   | is_ratpolyexp (Const ("Rings.divide_class.divide",_) $ t1 $ t2) = 
                ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
@@ -127,7 +127,7 @@
     if TermC.is_num' id 
     then (id |> TermC.int_opt_of_string |> the |> curry op * c, es) (*several numerals in one monom*)
     else (c, list_update es (find_index (curry op = t) vs) 1)
-  | monom_of_term  vs (c, es) (Const ("Prog_Expr.pow", _) $ (t as Free _) $ Free (e, _)) =
+  | monom_of_term  vs (c, es) (Const ("Transcendental.powr", _) $ (t as Free _) $ Free (e, _)) =
     (c, list_update es (find_index (curry op = t) vs) (the (TermC.int_opt_of_string e)))
   | monom_of_term vs (c, es) (Const ("Groups.times_class.times", _) $ m1 $ m2) =
     let val (c', es') = monom_of_term vs (c, es) m1
@@ -138,7 +138,7 @@
     [monom_of_term  vs (1, replicate (length vs) 0) t]
   | monoms_of_term vs (t as Free _) =
     [monom_of_term  vs (1, replicate (length vs) 0) t]
-  | monoms_of_term vs (t as Const ("Prog_Expr.pow", _) $ _ $  _) =
+  | monoms_of_term vs (t as Const ("Transcendental.powr", _) $ _ $  _) =
     [monom_of_term  vs (1, replicate (length vs) 0) t]
   | monoms_of_term vs (t as Const ("Groups.times_class.times", _) $ _ $  _) =
     [monom_of_term  vs (1, replicate (length vs) 0) t]
@@ -179,7 +179,7 @@
   | term_of_es baseT expT (_ :: vs) (0 :: es) = [] @ term_of_es baseT expT vs es
   | term_of_es baseT expT (v :: vs) (1 :: es) = v :: term_of_es baseT expT vs es
   | term_of_es baseT expT (v :: vs) (e :: es) =
-    Const ("Prog_Expr.pow", [baseT, expT] ---> baseT) $ v $  (Free (TermC.isastr_of_int e, expT))
+    Const ("Transcendental.powr", [baseT, expT] ---> baseT) $ v $  (Free (TermC.isastr_of_int e, expT))
     :: term_of_es baseT expT vs es
   | term_of_es _ _ _ _ = raise ERROR "term_of_es: length vs <> length es"
 
@@ -516,7 +516,7 @@
 	  [("PLUS", ("Groups.plus_class.plus", (**)eval_binop "#add_")),
 	  ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
 	  ("DIVIDE", ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")),
-	  ("POWER", ("Prog_Expr.pow", (**)eval_binop "#power_"))],
+	  ("POWER", ("Transcendental.powr", (**)eval_binop "#power_"))],
     errpatts = [],
 	scr =
 	  Rule.Rfuns {init_state  = init_state thy Atools_erls ro,
@@ -583,7 +583,7 @@
     calc = [("PLUS", ("Groups.plus_class.plus", (**)eval_binop "#add_")),
       ("TIMES", ("Groups.times_class.times", (**)eval_binop "#mult_")),
       ("DIVIDE", ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")),
-      ("POWER", ("Prog_Expr.pow", (**)eval_binop "#power_"))],
+      ("POWER", ("Transcendental.powr", (**)eval_binop "#power_"))],
     errpatts = [],
     scr = Rule.Rfuns {init_state  = init_state thy Atools_erls ro,
       normal_form = add_fraction_p_ thy,