neuper@37906
|
1 |
(* collecting all knowledge for Root
|
neuper@37906
|
2 |
created by:
|
neuper@37906
|
3 |
date:
|
neuper@37906
|
4 |
changed by: rlang
|
neuper@37906
|
5 |
last change by: rlang
|
neuper@37906
|
6 |
date: 02.10.24
|
neuper@37906
|
7 |
*)
|
neuper@37906
|
8 |
|
neuper@37906
|
9 |
(* use"../knowledge/Root.ML";
|
neuper@37947
|
10 |
use"Knowledge/Root.ML";
|
neuper@37906
|
11 |
use"Root.ML";
|
neuper@37906
|
12 |
|
neuper@37906
|
13 |
remove_thy"Root";
|
neuper@37947
|
14 |
use_thy"Knowledge/Isac";
|
neuper@37906
|
15 |
|
neuper@37906
|
16 |
use"ROOT.ML";
|
neuper@37906
|
17 |
cd"knowledge";
|
neuper@37906
|
18 |
*)
|
neuper@37906
|
19 |
"******* Root.ML begin *******";
|
neuper@37906
|
20 |
theory' := overwritel (!theory', [("Root.thy",Root.thy)]);
|
neuper@37906
|
21 |
(*-------------------------functions---------------------*)
|
neuper@37906
|
22 |
(*evaluation square-root over the integers*)
|
neuper@37906
|
23 |
fun eval_sqrt (thmid:string) (op_:string) (t as
|
neuper@37906
|
24 |
(Const(op0,t0) $ arg)) thy =
|
neuper@37906
|
25 |
(case arg of
|
neuper@37906
|
26 |
Free (n1,t1) =>
|
neuper@37906
|
27 |
(case int_of_str n1 of
|
neuper@37926
|
28 |
SOME ni =>
|
neuper@37926
|
29 |
if ni < 0 then NONE
|
neuper@37906
|
30 |
else
|
neuper@37906
|
31 |
let val fact = squfact ni;
|
neuper@37906
|
32 |
in if fact*fact = ni
|
neuper@37926
|
33 |
then SOME ("#sqrt #"^(string_of_int ni)^" = #"
|
neuper@37906
|
34 |
^(string_of_int (if ni = 0 then 0
|
neuper@37906
|
35 |
else ni div fact)),
|
neuper@37906
|
36 |
Trueprop $ mk_equality (t, term_of_num t1 fact))
|
neuper@37926
|
37 |
else if fact = 1 then NONE
|
neuper@37926
|
38 |
else SOME ("#sqrt #"^(string_of_int ni)^" = sqrt (#"
|
neuper@37906
|
39 |
^(string_of_int fact)^" * #"
|
neuper@37906
|
40 |
^(string_of_int fact)^" * #"
|
neuper@37906
|
41 |
^(string_of_int (ni div (fact*fact))^")"),
|
neuper@37906
|
42 |
Trueprop $
|
neuper@37906
|
43 |
(mk_equality
|
neuper@37906
|
44 |
(t,
|
neuper@37906
|
45 |
(mk_factroot op0 t1 fact
|
neuper@37906
|
46 |
(ni div (fact*fact))))))
|
neuper@37906
|
47 |
end
|
neuper@37926
|
48 |
| NONE => NONE)
|
neuper@37926
|
49 |
| _ => NONE)
|
neuper@37906
|
50 |
|
neuper@37926
|
51 |
| eval_sqrt _ _ _ _ = NONE;
|
neuper@37906
|
52 |
(*val (thmid, op_, t as Const(op0,t0) $ arg) = ("","", str2term "sqrt 0");
|
neuper@37906
|
53 |
> eval_sqrt thmid op_ t thy;
|
neuper@37906
|
54 |
> val Free (n1,t1) = arg;
|
neuper@37926
|
55 |
> val SOME ni = int_of_str n1;
|
neuper@37906
|
56 |
*)
|
neuper@37906
|
57 |
|
neuper@37906
|
58 |
calclist':= overwritel (!calclist',
|
neuper@37922
|
59 |
[("SQRT" ,("Root.sqrt" ,eval_sqrt "#sqrt_"))
|
neuper@37906
|
60 |
(*different types for 'sqrt 4' --- 'Calculate sqrt_'*)
|
neuper@37906
|
61 |
]);
|
neuper@37906
|
62 |
|
neuper@37906
|
63 |
|
neuper@37906
|
64 |
local (* Vers. 7.10.99.A *)
|
neuper@37906
|
65 |
|
neuper@37906
|
66 |
open Term; (* for type order = EQUAL | LESS | GREATER *)
|
neuper@37906
|
67 |
|
neuper@37906
|
68 |
fun pr_ord EQUAL = "EQUAL"
|
neuper@37906
|
69 |
| pr_ord LESS = "LESS"
|
neuper@37906
|
70 |
| pr_ord GREATER = "GREATER";
|
neuper@37906
|
71 |
|
neuper@37906
|
72 |
fun dest_hd' (Const (a, T)) = (* ~ term.ML *)
|
neuper@37906
|
73 |
(case a of "Root.sqrt" => ((("|||", 0), T), 0) (*WN greatest *)
|
neuper@37906
|
74 |
| _ => (((a, 0), T), 0))
|
neuper@37906
|
75 |
| dest_hd' (Free (a, T)) = (((a, 0), T), 1)
|
neuper@37906
|
76 |
| dest_hd' (Var v) = (v, 2)
|
neuper@37906
|
77 |
| dest_hd' (Bound i) = ((("", i), dummyT), 3)
|
neuper@37906
|
78 |
| dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4);
|
neuper@37906
|
79 |
fun size_of_term' (Const(str,_) $ t) =
|
neuper@37906
|
80 |
(case str of "Root.sqrt" => (1000 + size_of_term' t)
|
neuper@37906
|
81 |
| _ => 1 + size_of_term' t)
|
neuper@37906
|
82 |
| size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
|
neuper@37906
|
83 |
| size_of_term' (f $ t) = size_of_term' f + size_of_term' t
|
neuper@37906
|
84 |
| size_of_term' _ = 1;
|
neuper@37906
|
85 |
fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
|
neuper@37906
|
86 |
(case term_ord' pr thy (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
|
neuper@37906
|
87 |
| term_ord' pr thy (t, u) =
|
neuper@37906
|
88 |
(if pr then
|
neuper@37906
|
89 |
let
|
neuper@37906
|
90 |
val (f, ts) = strip_comb t and (g, us) = strip_comb u;
|
neuper@37906
|
91 |
val _=writeln("t= f@ts= \""^
|
neuper@37938
|
92 |
((Syntax.string_of_term (thy2ctxt thy)) f)^"\" @ \"["^
|
neuper@37938
|
93 |
(commas(map(Syntax.string_of_term (thy2ctxt thy)) ts))^"]\"");
|
neuper@37906
|
94 |
val _=writeln("u= g@us= \""^
|
neuper@37938
|
95 |
((Syntax.string_of_term (thy2ctxt thy)) g)^"\" @ \"["^
|
neuper@37938
|
96 |
(commas(map(Syntax.string_of_term (thy2ctxt thy)) us))^"]\"");
|
neuper@37906
|
97 |
val _=writeln("size_of_term(t,u)= ("^
|
neuper@37906
|
98 |
(string_of_int(size_of_term' t))^", "^
|
neuper@37906
|
99 |
(string_of_int(size_of_term' u))^")");
|
neuper@37906
|
100 |
val _=writeln("hd_ord(f,g) = "^((pr_ord o hd_ord)(f,g)));
|
neuper@37906
|
101 |
val _=writeln("terms_ord(ts,us) = "^
|
neuper@37906
|
102 |
((pr_ord o terms_ord str false)(ts,us)));
|
neuper@37906
|
103 |
val _=writeln("-------");
|
neuper@37906
|
104 |
in () end
|
neuper@37906
|
105 |
else ();
|
neuper@37906
|
106 |
case int_ord (size_of_term' t, size_of_term' u) of
|
neuper@37906
|
107 |
EQUAL =>
|
neuper@37906
|
108 |
let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
|
neuper@37906
|
109 |
(case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us)
|
neuper@37906
|
110 |
| ord => ord)
|
neuper@37906
|
111 |
end
|
neuper@37906
|
112 |
| ord => ord)
|
neuper@37906
|
113 |
and hd_ord (f, g) = (* ~ term.ML *)
|
neuper@37906
|
114 |
prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd' f, dest_hd' g)
|
neuper@37906
|
115 |
and terms_ord str pr (ts, us) =
|
neuper@37906
|
116 |
list_ord (term_ord' pr (assoc_thy "Isac.thy"))(ts, us);
|
neuper@37906
|
117 |
|
neuper@37906
|
118 |
in
|
neuper@37906
|
119 |
(* associates a+(b+c) => (a+b)+c = a+b+c ... avoiding parentheses
|
neuper@37906
|
120 |
by (1) size_of_term: less(!) to right, size_of 'sqrt (...)' = 1
|
neuper@37906
|
121 |
(2) hd_ord: greater to right, 'sqrt' < numerals < variables
|
neuper@37906
|
122 |
(3) terms_ord: recurs. on args, greater to right
|
neuper@37906
|
123 |
*)
|
neuper@37906
|
124 |
|
neuper@37906
|
125 |
(*args
|
neuper@37906
|
126 |
pr: print trace, WN0509 'sqrt_right true' not used anymore
|
neuper@37906
|
127 |
thy:
|
neuper@37906
|
128 |
subst: no bound variables, only Root.sqrt
|
neuper@37906
|
129 |
tu: the terms to compare (t1, t2) ... *)
|
neuper@37906
|
130 |
fun sqrt_right (pr:bool) thy (_:subst) tu =
|
neuper@37906
|
131 |
(term_ord' pr thy(***) tu = LESS );
|
neuper@37906
|
132 |
end;
|
neuper@37906
|
133 |
|
neuper@37906
|
134 |
rew_ord' := overwritel (!rew_ord',
|
neuper@37906
|
135 |
[("termlessI", termlessI),
|
neuper@37935
|
136 |
("sqrt_right", sqrt_right false (theory "Pure"))
|
neuper@37906
|
137 |
]);
|
neuper@37906
|
138 |
|
neuper@37906
|
139 |
(*-------------------------rulse-------------------------*)
|
neuper@37906
|
140 |
val Root_crls =
|
neuper@37906
|
141 |
append_rls "Root_crls" Atools_erls
|
neuper@37906
|
142 |
[Thm ("real_unari_minus",num_str real_unari_minus),
|
neuper@37906
|
143 |
Calc ("Root.sqrt" ,eval_sqrt "#sqrt_"),
|
neuper@37906
|
144 |
Calc ("HOL.divide",eval_cancel "#divide_"),
|
neuper@37906
|
145 |
Calc ("Atools.pow" ,eval_binop "#power_"),
|
neuper@37906
|
146 |
Calc ("op +", eval_binop "#add_"),
|
neuper@37906
|
147 |
Calc ("op -", eval_binop "#sub_"),
|
neuper@37906
|
148 |
Calc ("op *", eval_binop "#mult_"),
|
neuper@37906
|
149 |
Calc ("op =",eval_equal "#equal_")
|
neuper@37906
|
150 |
];
|
neuper@37906
|
151 |
|
neuper@37906
|
152 |
val Root_erls =
|
neuper@37906
|
153 |
append_rls "Root_erls" Atools_erls
|
neuper@37906
|
154 |
[Thm ("real_unari_minus",num_str real_unari_minus),
|
neuper@37906
|
155 |
Calc ("Root.sqrt" ,eval_sqrt "#sqrt_"),
|
neuper@37906
|
156 |
Calc ("HOL.divide",eval_cancel "#divide_"),
|
neuper@37906
|
157 |
Calc ("Atools.pow" ,eval_binop "#power_"),
|
neuper@37906
|
158 |
Calc ("op +", eval_binop "#add_"),
|
neuper@37906
|
159 |
Calc ("op -", eval_binop "#sub_"),
|
neuper@37906
|
160 |
Calc ("op *", eval_binop "#mult_"),
|
neuper@37906
|
161 |
Calc ("op =",eval_equal "#equal_")
|
neuper@37906
|
162 |
];
|
neuper@37906
|
163 |
|
neuper@37906
|
164 |
ruleset' := overwritelthy thy (!ruleset',
|
neuper@37906
|
165 |
[("Root_erls",Root_erls) (*FIXXXME:del with rls.rls'*)
|
neuper@37906
|
166 |
]);
|
neuper@37906
|
167 |
|
neuper@37906
|
168 |
val make_rooteq = prep_rls(
|
neuper@37906
|
169 |
Rls{id = "make_rooteq", preconds = []:term list,
|
neuper@37906
|
170 |
rew_ord = ("sqrt_right", sqrt_right false Root.thy),
|
neuper@37906
|
171 |
erls = Atools_erls, srls = Erls,
|
neuper@37906
|
172 |
calc = [],
|
neuper@37906
|
173 |
(*asm_thm = [],*)
|
neuper@37906
|
174 |
rules = [Thm ("real_diff_minus",num_str real_diff_minus),
|
neuper@37906
|
175 |
(*"a - b = a + (-1) * b"*)
|
neuper@37906
|
176 |
|
neuper@37906
|
177 |
Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib),
|
neuper@37906
|
178 |
(*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
|
neuper@37906
|
179 |
Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2),
|
neuper@37906
|
180 |
(*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
|
neuper@37906
|
181 |
Thm ("real_diff_mult_distrib" ,num_str real_diff_mult_distrib),
|
neuper@37906
|
182 |
(*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
|
neuper@37906
|
183 |
Thm ("real_diff_mult_distrib2",num_str real_diff_mult_distrib2),
|
neuper@37906
|
184 |
(*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
|
neuper@37906
|
185 |
|
neuper@37906
|
186 |
Thm ("real_mult_1",num_str real_mult_1),
|
neuper@37906
|
187 |
(*"1 * z = z"*)
|
neuper@37906
|
188 |
Thm ("real_mult_0",num_str real_mult_0),
|
neuper@37906
|
189 |
(*"0 * z = 0"*)
|
neuper@37906
|
190 |
Thm ("real_add_zero_left",num_str real_add_zero_left),
|
neuper@37906
|
191 |
(*"0 + z = z"*)
|
neuper@37906
|
192 |
|
neuper@37906
|
193 |
Thm ("real_mult_commute",num_str real_mult_commute), (*AC-rewriting*)
|
neuper@37906
|
194 |
Thm ("real_mult_left_commute",num_str real_mult_left_commute), (**)
|
neuper@37906
|
195 |
Thm ("real_mult_assoc",num_str real_mult_assoc), (**)
|
neuper@37906
|
196 |
Thm ("real_add_commute",num_str real_add_commute), (**)
|
neuper@37906
|
197 |
Thm ("real_add_left_commute",num_str real_add_left_commute), (**)
|
neuper@37906
|
198 |
Thm ("real_add_assoc",num_str real_add_assoc), (**)
|
neuper@37906
|
199 |
|
neuper@37906
|
200 |
Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)),
|
neuper@37906
|
201 |
(*"r1 * r1 = r1 ^^^ 2"*)
|
neuper@37906
|
202 |
Thm ("realpow_plus_1",num_str realpow_plus_1),
|
neuper@37906
|
203 |
(*"r * r ^^^ n = r ^^^ (n + 1)"*)
|
neuper@37906
|
204 |
Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),
|
neuper@37906
|
205 |
(*"z1 + z1 = 2 * z1"*)
|
neuper@37906
|
206 |
Thm ("real_mult_2_assoc",num_str real_mult_2_assoc),
|
neuper@37906
|
207 |
(*"z1 + (z1 + k) = 2 * z1 + k"*)
|
neuper@37906
|
208 |
|
neuper@37906
|
209 |
Thm ("real_num_collect",num_str real_num_collect),
|
neuper@37906
|
210 |
(*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*)
|
neuper@37906
|
211 |
Thm ("real_num_collect_assoc",num_str real_num_collect_assoc),
|
neuper@37906
|
212 |
(*"[| l is_const; m is_const |] ==> l * n + (m * n + k) = (l + m) * n + k"*)
|
neuper@37906
|
213 |
Thm ("real_one_collect",num_str real_one_collect),
|
neuper@37906
|
214 |
(*"m is_const ==> n + m * n = (1 + m) * n"*)
|
neuper@37906
|
215 |
Thm ("real_one_collect_assoc",num_str real_one_collect_assoc),
|
neuper@37906
|
216 |
(*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
|
neuper@37906
|
217 |
|
neuper@37906
|
218 |
Calc ("op +", eval_binop "#add_"),
|
neuper@37906
|
219 |
Calc ("op *", eval_binop "#mult_"),
|
neuper@37906
|
220 |
Calc ("Atools.pow", eval_binop "#power_")
|
neuper@37906
|
221 |
],
|
neuper@37906
|
222 |
scr = Script ((term_of o the o (parse thy)) "empty_script")
|
neuper@37906
|
223 |
}:rls);
|
neuper@37906
|
224 |
ruleset' := overwritelthy thy (!ruleset',
|
neuper@37906
|
225 |
[("make_rooteq", make_rooteq)
|
neuper@37906
|
226 |
]);
|
neuper@37906
|
227 |
|
neuper@37906
|
228 |
val expand_rootbinoms = prep_rls(
|
neuper@37906
|
229 |
Rls{id = "expand_rootbinoms", preconds = [],
|
neuper@37906
|
230 |
rew_ord = ("termlessI",termlessI),
|
neuper@37906
|
231 |
erls = Atools_erls, srls = Erls,
|
neuper@37906
|
232 |
calc = [],
|
neuper@37906
|
233 |
(*asm_thm = [],*)
|
neuper@37906
|
234 |
rules = [Thm ("real_plus_binom_pow2" ,num_str real_plus_binom_pow2),
|
neuper@37906
|
235 |
(*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*)
|
neuper@37906
|
236 |
Thm ("real_plus_binom_times" ,num_str real_plus_binom_times),
|
neuper@37906
|
237 |
(*"(a + b)*(a + b) = ...*)
|
neuper@37906
|
238 |
Thm ("real_minus_binom_pow2" ,num_str real_minus_binom_pow2),
|
neuper@37906
|
239 |
(*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*)
|
neuper@37906
|
240 |
Thm ("real_minus_binom_times",num_str real_minus_binom_times),
|
neuper@37906
|
241 |
(*"(a - b)*(a - b) = ...*)
|
neuper@37906
|
242 |
Thm ("real_plus_minus_binom1",num_str real_plus_minus_binom1),
|
neuper@37906
|
243 |
(*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*)
|
neuper@37906
|
244 |
Thm ("real_plus_minus_binom2",num_str real_plus_minus_binom2),
|
neuper@37906
|
245 |
(*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*)
|
neuper@37906
|
246 |
(*RL 020915*)
|
neuper@37906
|
247 |
Thm ("real_pp_binom_times",num_str real_pp_binom_times),
|
neuper@37906
|
248 |
(*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
|
neuper@37906
|
249 |
Thm ("real_pm_binom_times",num_str real_pm_binom_times),
|
neuper@37906
|
250 |
(*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
|
neuper@37906
|
251 |
Thm ("real_mp_binom_times",num_str real_mp_binom_times),
|
neuper@37906
|
252 |
(*(a - b)*(c p d) = a*c + a*d - b*c - b*d*)
|
neuper@37906
|
253 |
Thm ("real_mm_binom_times",num_str real_mm_binom_times),
|
neuper@37906
|
254 |
(*(a - b)*(c p d) = a*c - a*d - b*c + b*d*)
|
neuper@37906
|
255 |
Thm ("realpow_mul",num_str realpow_mul),
|
neuper@37906
|
256 |
(*(a*b)^^^n = a^^^n * b^^^n*)
|
neuper@37906
|
257 |
|
neuper@37906
|
258 |
Thm ("real_mult_1",num_str real_mult_1), (*"1 * z = z"*)
|
neuper@37906
|
259 |
Thm ("real_mult_0",num_str real_mult_0), (*"0 * z = 0"*)
|
neuper@37906
|
260 |
Thm ("real_add_zero_left",num_str real_add_zero_left), (*"0 + z = z"*)
|
neuper@37906
|
261 |
|
neuper@37906
|
262 |
Calc ("op +", eval_binop "#add_"),
|
neuper@37906
|
263 |
Calc ("op -", eval_binop "#sub_"),
|
neuper@37906
|
264 |
Calc ("op *", eval_binop "#mult_"),
|
neuper@37906
|
265 |
Calc ("HOL.divide" ,eval_cancel "#divide_"),
|
neuper@37906
|
266 |
Calc ("Root.sqrt",eval_sqrt "#sqrt_"),
|
neuper@37906
|
267 |
Calc ("Atools.pow", eval_binop "#power_"),
|
neuper@37906
|
268 |
|
neuper@37906
|
269 |
Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)),
|
neuper@37906
|
270 |
(*"r1 * r1 = r1 ^^^ 2"*)
|
neuper@37906
|
271 |
Thm ("realpow_plus_1",num_str realpow_plus_1),
|
neuper@37906
|
272 |
(*"r * r ^^^ n = r ^^^ (n + 1)"*)
|
neuper@37906
|
273 |
Thm ("real_mult_2_assoc",num_str real_mult_2_assoc),
|
neuper@37906
|
274 |
(*"z1 + (z1 + k) = 2 * z1 + k"*)
|
neuper@37906
|
275 |
|
neuper@37906
|
276 |
Thm ("real_num_collect",num_str real_num_collect),
|
neuper@37906
|
277 |
(*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*)
|
neuper@37906
|
278 |
Thm ("real_num_collect_assoc",num_str real_num_collect_assoc),
|
neuper@37906
|
279 |
(*"[| l is_const; m is_const |] ==> l * n + (m * n + k) = (l + m) * n + k"*)
|
neuper@37906
|
280 |
Thm ("real_one_collect",num_str real_one_collect),
|
neuper@37906
|
281 |
(*"m is_const ==> n + m * n = (1 + m) * n"*)
|
neuper@37906
|
282 |
Thm ("real_one_collect_assoc",num_str real_one_collect_assoc),
|
neuper@37906
|
283 |
(*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
|
neuper@37906
|
284 |
|
neuper@37906
|
285 |
Calc ("op +", eval_binop "#add_"),
|
neuper@37906
|
286 |
Calc ("op -", eval_binop "#sub_"),
|
neuper@37906
|
287 |
Calc ("op *", eval_binop "#mult_"),
|
neuper@37906
|
288 |
Calc ("HOL.divide" ,eval_cancel "#divide_"),
|
neuper@37906
|
289 |
Calc ("Root.sqrt",eval_sqrt "#sqrt_"),
|
neuper@37906
|
290 |
Calc ("Atools.pow", eval_binop "#power_")
|
neuper@37906
|
291 |
],
|
neuper@37906
|
292 |
scr = Script ((term_of o the o (parse thy)) "empty_script")
|
neuper@37906
|
293 |
}:rls);
|
neuper@37906
|
294 |
|
neuper@37906
|
295 |
|
neuper@37906
|
296 |
ruleset' := overwritelthy thy (!ruleset',
|
neuper@37906
|
297 |
[("expand_rootbinoms", expand_rootbinoms)
|
neuper@37906
|
298 |
]);
|
neuper@37906
|
299 |
"******* Root.ML end *******";
|