equal
deleted
inserted
replaced
15 merge_rls "rootrat_erls" Root_erls |
15 merge_rls "rootrat_erls" Root_erls |
16 (merge_rls "" rational_erls |
16 (merge_rls "" rational_erls |
17 (append_rls "" e_rls |
17 (append_rls "" e_rls |
18 [])); |
18 [])); |
19 |
19 |
20 ruleset' := overwritelthy thy (!ruleset', |
20 ruleset' := overwritelthy @{theory} (!ruleset', |
21 [("rootrat_erls",rootrat_erls) (*FIXXXME:del with rls.rls'*)]); |
21 [("rootrat_erls",rootrat_erls) (*FIXXXME:del with rls.rls'*)]); |
22 |
22 |
23 (*.calculate numeral groundterms.*) |
23 (*.calculate numeral groundterms.*) |
24 val calculate_RootRat = |
24 val calculate_RootRat = |
25 append_rls "calculate_RootRat" calculate_Rational |
25 append_rls "calculate_RootRat" calculate_Rational |
29 (* 1 * z = z *) |
29 (* 1 * z = z *) |
30 Thm ("sym_real_mult_minus1",num_str @{(real_mult_minus1 RS sym)), |
30 Thm ("sym_real_mult_minus1",num_str @{(real_mult_minus1 RS sym)), |
31 (* "- z1 = -1 * z1" *) |
31 (* "- z1 = -1 * z1" *) |
32 Calc ("Root.sqrt",eval_sqrt "#sqrt_") |
32 Calc ("Root.sqrt",eval_sqrt "#sqrt_") |
33 ]; |
33 ]; |
34 ruleset' := overwritelthy thy (!ruleset', |
34 ruleset' := overwritelthy @{theory} (!ruleset', |
35 [("calculate_RootRat",calculate_RootRat)]); |
35 [("calculate_RootRat",calculate_RootRat)]); |
36 *} |
36 *} |
37 |
37 |
38 end |
38 end |