1.1 --- a/test/Tools/isac/ProgLang/evaluate.sml Wed Aug 24 18:29:33 2022 +0200
1.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml Wed Aug 24 19:02:19 2022 +0200
1.3 @@ -49,10 +49,10 @@
1.4 val t = TermC.str2term "((1+2)*4/3) \<up> 2";
1.5 val thy = @{theory};
1.6 val ctxt = Proof_Context.init_global @{theory}
1.7 -val times = ("Groups.times_class.times", Calc_Binop.numeric "#mult_") : string * Eval_Def.ml_fun;
1.8 -val plus = ("Groups.plus_class.plus", Calc_Binop.numeric "#add_") : string * Eval_Def.ml_fun;
1.9 -val divide = ("Rings.divide_class.divide", eval_cancel "#divide_e") : string * Eval_Def.ml_fun;
1.10 -val pow = (\<^const_name>\<open>realpow\<close>, Calc_Binop.numeric "#power_") : string * Eval_Def.ml_fun;
1.11 +val times = ("Groups.times_class.times", Calc_Binop.numeric "#mult_") : string * Eval.ml_fun;
1.12 +val plus = ("Groups.plus_class.plus", Calc_Binop.numeric "#add_") : string * Eval.ml_fun;
1.13 +val divide = ("Rings.divide_class.divide", eval_cancel "#divide_e") : string * Eval.ml_fun;
1.14 +val pow = (\<^const_name>\<open>realpow\<close>, Calc_Binop.numeric "#power_") : string * Eval.ml_fun;
1.15
1.16 "~~~~~ fun calculate_ , args:"; val (thy, isa_fn, t) = (thy, plus, t);
1.17 val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{context} isa_fn t;