101 [("#Given" ,["realTestGiven t_"]), |
101 [("#Given" ,["realTestGiven t_"]), |
102 ("#Find" ,["realTestFind s_"]) |
102 ("#Find" ,["realTestFind s_"]) |
103 ], |
103 ], |
104 {rew_ord'="sqrt_right",rls'=tval_rls,srls=e_rls,prls=e_rls, |
104 {rew_ord'="sqrt_right",rls'=tval_rls,srls=e_rls,prls=e_rls, |
105 calc=[("PLUS" ,("op +" ,eval_binop "#add_")), |
105 calc=[("PLUS" ,("op +" ,eval_binop "#add_")), |
106 ("TIMES" ,("op *" ,eval_binop "#mult_")), |
106 ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")), |
107 ("DIVIDE" ,("HOL.divide" ,eval_cancel "#divide_")), |
107 ("DIVIDE" ,("HOL.divide" ,eval_cancel "#divide_")), |
108 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))], |
108 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))], |
109 crls=tval_rls, nrls=e_rls(*, |
109 crls=tval_rls, nrls=e_rls(*, |
110 asm_rls=[],asm_thm=[]*)}, |
110 asm_rls=[],asm_thm=[]*)}, |
111 "Script STest_simplify (t_::real) = \ |
111 "Script STest_simplify (t_::real) = \ |