1.1 --- a/test/Tools/isac/ProgLang/evaluate.sml	Thu Aug 04 16:48:37 2022 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml	Fri Aug 05 08:45:37 2022 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4  "----------- check calculate bottom up -----------------";
     1.5  "----------- Prog_Expr.pow Power.power_class.power ---------";
     1.6  "----------- fun cancel_int --------------------------------------------------------------------";
     1.7 -"----------- RE-BUILD fun calcul ---------------------------------------------------------------";
     1.8 +"----------- RE-BUILD fun Calc_Binop.simplify ---------------------------------------------------------------";
     1.9  "----------- get_pair with 3 args -----------------------";
    1.10  "----------- calculate (2 * x is_num) -------------------";
    1.11  "----------- fun get_pair: examples ------------------------------------------------------------";
    1.12 @@ -49,10 +49,10 @@
    1.13  val t = TermC.str2term "((1+2)*4/3) \<up> 2";
    1.14  val thy = @{theory};
    1.15  val ctxt = Proof_Context.init_global @{theory}
    1.16 -val times =  ("Groups.times_class.times", eval_binop "#mult_") : string * Eval_Def.eval_fn;
    1.17 -val plus =   ("Groups.plus_class.plus", eval_binop "#add_") : string * Eval_Def.eval_fn;
    1.18 +val times =  ("Groups.times_class.times", Calc_Binop.numeric "#mult_") : string * Eval_Def.eval_fn;
    1.19 +val plus =   ("Groups.plus_class.plus", Calc_Binop.numeric "#add_") : string * Eval_Def.eval_fn;
    1.20  val divide = ("Rings.divide_class.divide", eval_cancel "#divide_e") : string * Eval_Def.eval_fn;
    1.21 -val pow =    (\<^const_name>\<open>realpow\<close>, eval_binop "#power_") : string * Eval_Def.eval_fn;
    1.22 +val pow =    (\<^const_name>\<open>realpow\<close>, Calc_Binop.numeric "#power_") : string * Eval_Def.eval_fn;
    1.23  
    1.24  "~~~~~ fun calculate_ , args:"; val (thy, isa_fn, t) = (thy, plus, t);
    1.25  val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{theory} isa_fn t;
    1.26 @@ -279,7 +279,7 @@
    1.27      Const (\<^const_name>\<open>realpow\<close>, _) $ (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _))) $
    1.28        (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit0\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _)))) => ()
    1.29  | _ => error "3 \<up> 2 CHANGED";
    1.30 -  val SOME (id, t') = eval_binop thmid op_ t ctxt;
    1.31 +  val SOME (id, t') = Calc_Binop.numeric thmid op_ t ctxt;
    1.32  (*** calc: operator = pow not defined*)
    1.33  
    1.34  if UnparseC.term t' = "3 \<up> 2 = 9" then () else error "eval_binop  3 \<up> 2 = 9  CHANGED";
    1.35 @@ -293,12 +293,12 @@
    1.36  if cancel_int (6, 4) = (1, (3, 2)) then () else error "cancel_int (6, 4)CHANGED";
    1.37  
    1.38  
    1.39 -"----------- RE-BUILD fun calcul ---------------------------------------------------------------";
    1.40 -"----------- RE-BUILD fun calcul ---------------------------------------------------------------";
    1.41 -"----------- RE-BUILD fun calcul ---------------------------------------------------------------";
    1.42 +"----------- RE-BUILD fun Calc_Binop.simplify ---------------------------------------------------------------";
    1.43 +"----------- RE-BUILD fun Calc_Binop.simplify ---------------------------------------------------------------";
    1.44 +"----------- RE-BUILD fun Calc_Binop.simplify ---------------------------------------------------------------";
    1.45  val t = @{term "2 + 3 ::real"};
    1.46  
    1.47 -"~~~~~ fun calcul , args:"; val (thy, lhs) = (@{theory}, t);
    1.48 +"~~~~~ fun Calc_Binop.simplify , args:"; val (thy, lhs) = (@{theory}, t);
    1.49      val simp_ctxt =
    1.50        Proof_Context.init_global thy
    1.51        |> put_simpset (Simplifier.simpset_of @{theory_context BaseDefinitions});