diff -r 5b1cd0f93d8b -r 98ee674d18d3 test/Tools/isac/ProgLang/evaluate.sml --- a/test/Tools/isac/ProgLang/evaluate.sml Sun May 02 15:55:37 2021 +0200 +++ b/test/Tools/isac/ProgLang/evaluate.sml Mon May 03 08:49:50 2021 +0200 @@ -48,7 +48,7 @@ val times = ("Groups.times_class.times", eval_binop "#mult_") : string * Eval_Def.eval_fn; val plus = ("Groups.plus_class.plus",eval_binop "#add_") : string * Eval_Def.eval_fn; val divide = ("Rings.divide_class.divide" ,eval_cancel "#divide_e") : string * Eval_Def.eval_fn; -val pow = ("Prog_Expr.pow" ,eval_binop "#power_") : string * Eval_Def.eval_fn; +val pow = ("Transcendental.powr" ,eval_binop "#power_") : string * Eval_Def.eval_fn; "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, plus, t); val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{theory} isa_fn t; @@ -282,7 +282,7 @@ val (op_, eval_fn) = the (LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER")); (* -val op_ = "Prog_Expr.pow" : string +val op_ = "Transcendental.powr" : string val eval_fn = fn : string -> term -> theory -> (string * term) option*) val SOME (thmid,t') = get_pair thy op_ eval_fn t;