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