equal
deleted
inserted
replaced
18 Rule_Set.append_rules "calculate_RootRat" calculate_Rational |
18 Rule_Set.append_rules "calculate_RootRat" calculate_Rational |
19 [\<^rule_thm>\<open>distrib_left\<close>, |
19 [\<^rule_thm>\<open>distrib_left\<close>, |
20 (* w*(z1.0 + z2.0) = w * z1.0 + w * z2.0 *) |
20 (* w*(z1.0 + z2.0) = w * z1.0 + w * z2.0 *) |
21 \<^rule_thm>\<open>mult_1_left\<close>, |
21 \<^rule_thm>\<open>mult_1_left\<close>, |
22 (* 1 * z = z *) |
22 (* 1 * z = z *) |
23 Rule.Thm ("real_mult_minus1_sym", ThmC.numerals_to_Free (@{thm real_mult_minus1_sym})), |
23 Rule.Thm ("real_mult_minus1_sym", (@{thm real_mult_minus1_sym})), |
24 (*"\<not>(z is_const) ==> - (z::real) = -1 * z"*) |
24 (*"\<not>(z is_const) ==> - (z::real) = -1 * z"*) |
25 Rule.Eval ("NthRoot.sqrt", eval_sqrt "#sqrt_") |
25 Rule.Eval ("NthRoot.sqrt", eval_sqrt "#sqrt_") |
26 ]; |
26 ]; |
27 |
27 |
28 val prep_rls' = Auto_Prog.prep_rls @{theory}; |
28 val prep_rls' = Auto_Prog.prep_rls @{theory}; |