src/Tools/isac/Knowledge/LinEq.thy
changeset 60405 d4ebe139100d
parent 60358 8377b6c37640
child 60449 2406d378cede
     1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Thu Sep 16 12:23:57 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Thu Sep 16 17:23:54 2021 +0200
     1.3 @@ -46,7 +46,7 @@
     1.4      (*		
     1.5       Don't use
     1.6       \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
     1.7 -     \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),
     1.8 +     \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
     1.9       *)
    1.10      ];
    1.11  
    1.12 @@ -57,7 +57,7 @@
    1.13      (*		
    1.14       Don't use
    1.15       \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
    1.16 -     \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),
    1.17 +     \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
    1.18       *)
    1.19      ];
    1.20  \<close>
    1.21 @@ -79,7 +79,7 @@
    1.22         \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
    1.23         \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
    1.24         *)
    1.25 -      \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_")],
    1.26 +      \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_")],
    1.27      scr = Rule.Empty_Prog});
    1.28  \<close>
    1.29  rule_set_knowledge LinPoly_simplify = LinPoly_simplify