1.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Sun May 02 15:55:37 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Mon May 03 08:49:50 2021 +0200
     1.3 @@ -25,7 +25,7 @@
     1.4    | is_ratpolyexp (Const ("Groups.plus_class.plus",_) $ Free _ $ Free _) = true
     1.5    | is_ratpolyexp (Const ("Groups.minus_class.minus",_) $ Free _ $ Free _) = true
     1.6    | is_ratpolyexp (Const ("Groups.times_class.times",_) $ Free _ $ Free _) = true
     1.7 -  | is_ratpolyexp (Const ("Prog_Expr.pow",_) $ Free _ $ Free _) = true
     1.8 +  | is_ratpolyexp (Const ("Transcendental.powr",_) $ Free _ $ Free _) = true
     1.9    | is_ratpolyexp (Const ("Rings.divide_class.divide",_) $ Free _ $ Free _) = true
    1.10    | is_ratpolyexp (Const ("Groups.plus_class.plus",_) $ t1 $ t2) = 
    1.11                 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
    1.12 @@ -33,7 +33,7 @@
    1.13                 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
    1.14    | is_ratpolyexp (Const ("Groups.times_class.times",_) $ t1 $ t2) = 
    1.15                 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
    1.16 -  | is_ratpolyexp (Const ("Prog_Expr.pow",_) $ t1 $ t2) = 
    1.17 +  | is_ratpolyexp (Const ("Transcendental.powr",_) $ t1 $ t2) = 
    1.18                 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
    1.19    | is_ratpolyexp (Const ("Rings.divide_class.divide",_) $ t1 $ t2) = 
    1.20                 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
    1.21 @@ -127,7 +127,7 @@
    1.22      if TermC.is_num' id 
    1.23      then (id |> TermC.int_opt_of_string |> the |> curry op * c, es) (*several numerals in one monom*)
    1.24      else (c, list_update es (find_index (curry op = t) vs) 1)
    1.25 -  | monom_of_term  vs (c, es) (Const ("Prog_Expr.pow", _) $ (t as Free _) $ Free (e, _)) =
    1.26 +  | monom_of_term  vs (c, es) (Const ("Transcendental.powr", _) $ (t as Free _) $ Free (e, _)) =
    1.27      (c, list_update es (find_index (curry op = t) vs) (the (TermC.int_opt_of_string e)))
    1.28    | monom_of_term vs (c, es) (Const ("Groups.times_class.times", _) $ m1 $ m2) =
    1.29      let val (c', es') = monom_of_term vs (c, es) m1
    1.30 @@ -138,7 +138,7 @@
    1.31      [monom_of_term  vs (1, replicate (length vs) 0) t]
    1.32    | monoms_of_term vs (t as Free _) =
    1.33      [monom_of_term  vs (1, replicate (length vs) 0) t]
    1.34 -  | monoms_of_term vs (t as Const ("Prog_Expr.pow", _) $ _ $  _) =
    1.35 +  | monoms_of_term vs (t as Const ("Transcendental.powr", _) $ _ $  _) =
    1.36      [monom_of_term  vs (1, replicate (length vs) 0) t]
    1.37    | monoms_of_term vs (t as Const ("Groups.times_class.times", _) $ _ $  _) =
    1.38      [monom_of_term  vs (1, replicate (length vs) 0) t]
    1.39 @@ -179,7 +179,7 @@
    1.40    | term_of_es baseT expT (_ :: vs) (0 :: es) = [] @ term_of_es baseT expT vs es
    1.41    | term_of_es baseT expT (v :: vs) (1 :: es) = v :: term_of_es baseT expT vs es
    1.42    | term_of_es baseT expT (v :: vs) (e :: es) =
    1.43 -    Const ("Prog_Expr.pow", [baseT, expT] ---> baseT) $ v $  (Free (TermC.isastr_of_int e, expT))
    1.44 +    Const ("Transcendental.powr", [baseT, expT] ---> baseT) $ v $  (Free (TermC.isastr_of_int e, expT))
    1.45      :: term_of_es baseT expT vs es
    1.46    | term_of_es _ _ _ _ = raise ERROR "term_of_es: length vs <> length es"
    1.47  
    1.48 @@ -516,7 +516,7 @@
    1.49  	  [("PLUS", ("Groups.plus_class.plus", (**)eval_binop "#add_")),
    1.50  	  ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
    1.51  	  ("DIVIDE", ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")),
    1.52 -	  ("POWER", ("Prog_Expr.pow", (**)eval_binop "#power_"))],
    1.53 +	  ("POWER", ("Transcendental.powr", (**)eval_binop "#power_"))],
    1.54      errpatts = [],
    1.55  	scr =
    1.56  	  Rule.Rfuns {init_state  = init_state thy Atools_erls ro,
    1.57 @@ -583,7 +583,7 @@
    1.58      calc = [("PLUS", ("Groups.plus_class.plus", (**)eval_binop "#add_")),
    1.59        ("TIMES", ("Groups.times_class.times", (**)eval_binop "#mult_")),
    1.60        ("DIVIDE", ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")),
    1.61 -      ("POWER", ("Prog_Expr.pow", (**)eval_binop "#power_"))],
    1.62 +      ("POWER", ("Transcendental.powr", (**)eval_binop "#power_"))],
    1.63      errpatts = [],
    1.64      scr = Rule.Rfuns {init_state  = init_state thy Atools_erls ro,
    1.65        normal_form = add_fraction_p_ thy,