diff -r 716f399db0a5 -r d4ebe139100d test/Tools/isac/ProgLang/evaluate.sml --- a/test/Tools/isac/ProgLang/evaluate.sml Thu Sep 16 12:23:57 2021 +0200 +++ b/test/Tools/isac/ProgLang/evaluate.sml Thu Sep 16 17:23:54 2021 +0200 @@ -51,7 +51,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 = ("Transcendental.powr", eval_binop "#power_") : string * Eval_Def.eval_fn; +val pow = (\<^const_name>\realpow\, 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; @@ -269,7 +269,7 @@ val (op_, eval_fn) = the (LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER")); (* -val op_ = \<^const_name>\powr\ : string +val op_ = \<^const_name>\realpow\ : string val eval_fn = fn : string -> term -> theory -> (string * term) option*) val SOME (thmid,t') = get_pair thy op_ eval_fn t; @@ -279,8 +279,8 @@ (*** calc: operator = pow not defined*) case (op_, t) of - ("Transcendental.powr", - Const (\<^const_name>\powr\, _) $ (Const (\<^const_name>\numeral\, _) $ (Const (\<^const_name>\num.Bit1\, _) $ Const (\<^const_name>\num.One\, _))) $ + (\<^const_name>\realpow\, + Const (\<^const_name>\realpow\, _) $ (Const (\<^const_name>\numeral\, _) $ (Const (\<^const_name>\num.Bit1\, _) $ Const (\<^const_name>\num.One\, _))) $ (Const (\<^const_name>\numeral\, _) $ (Const (\<^const_name>\num.Bit0\, _) $ Const (\<^const_name>\num.One\, _)))) => () | _ => error "3 \ 2 CHANGED"; val SOME (id, t') = eval_binop thmid op_ t thy;