38 Calc ("Tools.rhs" ,eval_rhs ""), |
38 Calc ("Tools.rhs" ,eval_rhs ""), |
39 Calc ("Poly.has'_degree'_in",eval_has_degree_in ""), |
39 Calc ("Poly.has'_degree'_in",eval_has_degree_in ""), |
40 Calc ("Poly.is'_polyrat'_in",eval_is_polyrat_in ""), |
40 Calc ("Poly.is'_polyrat'_in",eval_is_polyrat_in ""), |
41 Calc ("Atools.occurs'_in",eval_occurs_in ""), |
41 Calc ("Atools.occurs'_in",eval_occurs_in ""), |
42 Calc ("Atools.ident",eval_ident "#ident_"), |
42 Calc ("Atools.ident",eval_ident "#ident_"), |
43 Thm ("not_true",num_str not_true), |
43 Thm ("not_true",num_str @{not_true), |
44 Thm ("not_false",num_str not_false), |
44 Thm ("not_false",num_str @{not_false), |
45 Thm ("and_true",num_str and_true), |
45 Thm ("and_true",num_str @{and_true), |
46 Thm ("and_false",num_str and_false), |
46 Thm ("and_false",num_str @{and_false), |
47 Thm ("or_true",num_str or_true), |
47 Thm ("or_true",num_str @{or_true), |
48 Thm ("or_false",num_str or_false) |
48 Thm ("or_false",num_str @{or_false) |
49 ]; |
49 ]; |
50 (* ----- erls ----- *) |
50 (* ----- erls ----- *) |
51 val LinEq_crls = |
51 val LinEq_crls = |
52 append_rls "LinEq_crls" poly_crls |
52 append_rls "LinEq_crls" poly_crls |
53 [Thm ("real_assoc_1",num_str real_assoc_1) |
53 [Thm ("real_assoc_1",num_str @{real_assoc_1) |
54 (* |
54 (* |
55 Don't use |
55 Don't use |
56 Calc ("HOL.divide", eval_cancel "#divide_"), |
56 Calc ("HOL.divide", eval_cancel "#divide_"), |
57 Calc ("Atools.pow" ,eval_binop "#power_"), |
57 Calc ("Atools.pow" ,eval_binop "#power_"), |
58 *) |
58 *) |
59 ]; |
59 ]; |
60 |
60 |
61 (* ----- crls ----- *) |
61 (* ----- crls ----- *) |
62 val LinEq_erls = |
62 val LinEq_erls = |
63 append_rls "LinEq_erls" Poly_erls |
63 append_rls "LinEq_erls" Poly_erls |
64 [Thm ("real_assoc_1",num_str real_assoc_1) |
64 [Thm ("real_assoc_1",num_str @{real_assoc_1) |
65 (* |
65 (* |
66 Don't use |
66 Don't use |
67 Calc ("HOL.divide", eval_cancel "#divide_"), |
67 Calc ("HOL.divide", eval_cancel "#divide_"), |
68 Calc ("Atools.pow" ,eval_binop "#power_"), |
68 Calc ("Atools.pow" ,eval_binop "#power_"), |
69 *) |
69 *) |
79 erls = LinEq_erls, |
79 erls = LinEq_erls, |
80 srls = Erls, |
80 srls = Erls, |
81 calc = [], |
81 calc = [], |
82 (*asm_thm = [],*) |
82 (*asm_thm = [],*) |
83 rules = [ |
83 rules = [ |
84 Thm ("real_assoc_1",num_str real_assoc_1), |
84 Thm ("real_assoc_1",num_str @{real_assoc_1), |
85 Calc ("op +",eval_binop "#add_"), |
85 Calc ("op +",eval_binop "#add_"), |
86 Calc ("op -",eval_binop "#sub_"), |
86 Calc ("op -",eval_binop "#sub_"), |
87 Calc ("op *",eval_binop "#mult_"), |
87 Calc ("op *",eval_binop "#mult_"), |
88 (* Dont use |
88 (* Dont use |
89 Calc ("HOL.divide", eval_cancel "#divide_"), |
89 Calc ("HOL.divide", eval_cancel "#divide_"), |
103 erls = LinEq_erls, |
103 erls = LinEq_erls, |
104 srls = Erls, |
104 srls = Erls, |
105 calc = [], |
105 calc = [], |
106 (*asm_thm = [("lin_isolate_div","")],*) |
106 (*asm_thm = [("lin_isolate_div","")],*) |
107 rules = [ |
107 rules = [ |
108 Thm("lin_isolate_add1",num_str lin_isolate_add1), |
108 Thm("lin_isolate_add1",num_str @{lin_isolate_add1), |
109 (* a+bx=0 -> bx=-a *) |
109 (* a+bx=0 -> bx=-a *) |
110 Thm("lin_isolate_add2",num_str lin_isolate_add2), |
110 Thm("lin_isolate_add2",num_str @{lin_isolate_add2), |
111 (* a+ x=0 -> x=-a *) |
111 (* a+ x=0 -> x=-a *) |
112 Thm("lin_isolate_div",num_str lin_isolate_div) |
112 Thm("lin_isolate_div",num_str @{lin_isolate_div) |
113 (* bx=c -> x=c/b *) |
113 (* bx=c -> x=c/b *) |
114 ], |
114 ], |
115 scr = Script ((term_of o the o (parse thy)) "empty_script") |
115 scr = Script ((term_of o the o (parse thy)) "empty_script") |
116 }:rls); |
116 }:rls); |
117 ruleset' := overwritelthy thy (!ruleset', |
117 ruleset' := overwritelthy thy (!ruleset', |