equal
deleted
inserted
replaced
23 Thm ("sym_real_mult_minus1",num_str (@{thm real_mult_minus1} RS @{thm sym})), |
23 Thm ("sym_real_mult_minus1",num_str (@{thm real_mult_minus1} RS @{thm sym})), |
24 (* "- z1 = -1 * z1" *) |
24 (* "- z1 = -1 * z1" *) |
25 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_") |
25 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_") |
26 ]; |
26 ]; |
27 |
27 |
28 val prep_rls' = prep_rls @{theory}; |
28 val prep_rls' = LTool.prep_rls @{theory}; |
29 *} |
29 *} |
30 setup {* KEStore_Elems.add_rlss |
30 setup {* KEStore_Elems.add_rlss |
31 [("rootrat_erls", (Context.theory_name @{theory}, prep_rls' rootrat_erls)), |
31 [("rootrat_erls", (Context.theory_name @{theory}, prep_rls' rootrat_erls)), |
32 ("calculate_RootRat", (Context.theory_name @{theory}, prep_rls' calculate_RootRat))] *} |
32 ("calculate_RootRat", (Context.theory_name @{theory}, prep_rls' calculate_RootRat))] *} |
33 |
33 |