|
1 (*.(c) by Richard Lang, 2003 .*) |
|
2 (* collecting all knowledge for Root and Rational |
|
3 created by: rlang |
|
4 date: 02.10 |
|
5 changed by: rlang |
|
6 last change by: rlang |
|
7 date: 02.10.21 |
|
8 *) |
|
9 (* use"knowledge/RootRat.ML"; |
|
10 use"RootRat.ML"; |
|
11 |
|
12 use"ROOT.ML"; |
|
13 cd"knowledge"; |
|
14 |
|
15 remove_thy"RootRat"; |
|
16 use_thy"Isac"; |
|
17 *) |
|
18 |
|
19 "******* RootRat.ML begin *******"; |
|
20 theory' := overwritel (!theory', [("RootRat.thy",RootRat.thy)]); |
|
21 |
|
22 (*-------------------------functions---------------------*) |
|
23 |
|
24 (*-------------------------rulse-------------------------*) |
|
25 val rootrat_erls = |
|
26 merge_rls "rootrat_erls" Root_erls |
|
27 (merge_rls "" rational_erls |
|
28 (append_rls "" e_rls |
|
29 [])); |
|
30 |
|
31 ruleset' := overwritelthy thy (!ruleset', |
|
32 [("rootrat_erls",rootrat_erls) (*FIXXXME:del with rls.rls'*) |
|
33 ]); |
|
34 |
|
35 (*.calculate numeral groundterms.*) |
|
36 val calculate_RootRat = |
|
37 append_rls "calculate_RootRat" calculate_Rational |
|
38 [Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2), |
|
39 (* w*(z1.0 + z2.0) = w * z1.0 + w * z2.0 *) |
|
40 Thm ("real_mult_1",num_str real_mult_1), |
|
41 (* 1 * z = z *) |
|
42 Thm ("sym_real_mult_minus1",num_str (real_mult_minus1 RS sym)), |
|
43 (* "- z1 = -1 * z1" *) |
|
44 Calc ("Root.sqrt",eval_sqrt "#sqrt_") |
|
45 ]; |
|
46 ruleset' := overwritelthy thy (!ruleset', |
|
47 [("calculate_RootRat",calculate_RootRat)]); |
|
48 |
|
49 |
|
50 "******* RootRat.ML end *******"; |