160 ("sqrt_right", sqrt_right false @{theory "Pure"}) |
160 ("sqrt_right", sqrt_right false @{theory "Pure"}) |
161 ]); |
161 ]); |
162 |
162 |
163 (*-------------------------rulse-------------------------*) |
163 (*-------------------------rulse-------------------------*) |
164 val Root_crls = |
164 val Root_crls = |
165 Rule_Set.append_rls "Root_crls" Atools_erls |
165 Rule_Set.append_rules "Root_crls" Atools_erls |
166 [Rule.Thm ("real_unari_minus",TermC.num_str @{thm real_unari_minus}), |
166 [Rule.Thm ("real_unari_minus",TermC.num_str @{thm real_unari_minus}), |
167 Rule.Num_Calc ("NthRoot.sqrt" , eval_sqrt "#sqrt_"), |
167 Rule.Num_Calc ("NthRoot.sqrt" , eval_sqrt "#sqrt_"), |
168 Rule.Num_Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"), |
168 Rule.Num_Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"), |
169 Rule.Num_Calc ("Prog_Expr.pow" , (**)eval_binop "#power_"), |
169 Rule.Num_Calc ("Prog_Expr.pow" , (**)eval_binop "#power_"), |
170 Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"), |
170 Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"), |
172 Rule.Num_Calc ("Groups.times_class.times", (**)eval_binop "#mult_"), |
172 Rule.Num_Calc ("Groups.times_class.times", (**)eval_binop "#mult_"), |
173 Rule.Num_Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_") |
173 Rule.Num_Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_") |
174 ]; |
174 ]; |
175 |
175 |
176 val Root_erls = |
176 val Root_erls = |
177 Rule_Set.append_rls "Root_erls" Atools_erls |
177 Rule_Set.append_rules "Root_erls" Atools_erls |
178 [Rule.Thm ("real_unari_minus",TermC.num_str @{thm real_unari_minus}), |
178 [Rule.Thm ("real_unari_minus",TermC.num_str @{thm real_unari_minus}), |
179 Rule.Num_Calc ("NthRoot.sqrt" , eval_sqrt "#sqrt_"), |
179 Rule.Num_Calc ("NthRoot.sqrt" , eval_sqrt "#sqrt_"), |
180 Rule.Num_Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"), |
180 Rule.Num_Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"), |
181 Rule.Num_Calc ("Prog_Expr.pow" , (**)eval_binop "#power_"), |
181 Rule.Num_Calc ("Prog_Expr.pow" , (**)eval_binop "#power_"), |
182 Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"), |
182 Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"), |