cleanup, naming: 'KEStore_Elems' in Tests now 'Test_KEStore_Elems', 'store_pbts' now 'add_pbts'
1 (* Title: test/Tools/isac/build_thydata.sml
2 Author: Walther Neuper, TU Graz, 2010
3 (c) due to copyright terms
5 12345678901234567890123456789012345678901234567890123456789012345678901234567890
6 10 20 30 40 50 60 70 80
9 "--------------------------------------------------------";
10 "--------------------------------------------------------";
11 "table of contents --------------------------------------";
12 "--------------------------------------------------------";
13 "-------- OLD compute rlsthmsNOTisac by eq_thmID --------";
14 "-------- retrieve isa-b/c theories from Isabelle -------";
15 "-------- prop_of thm .. Theory.axioms_of ---------------";
16 "-------- compute val rlsthmsNOTisac --------------------";
17 "-------- hard-coded val rlsthmsNOTisac -----------------";
18 "-------- the_hier (! thehier) (collect_thydata ())------";
19 "-------- retrieve errpats ------------------------------";
20 "--------------------------------------------------------";
21 "--------------------------------------------------------";
22 "--------------------------------------------------------";
24 "-------- OLD compute rlsthmsNOTisac by eq_thmID --------";
25 "-------- OLD compute rlsthmsNOTisac by eq_thmID --------";
26 "-------- OLD compute rlsthmsNOTisac by eq_thmID --------";
28 view src/Pure/isac/IsacKnowledge/Isac.ML @ 37874:331e38464ada
29 date Thu Jul 22 10:45:18 2010 +0200
32 val isacrlsthms = ((gen_distinct eq_thmI) o (map rep_thm_G') o flat o
33 (map (thms_of_rls o #2 o #2))) (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"));
34 val isacthms = (flat o (map (thms_of o #2))) (!theory');
36 val rlsthmsNOTisac = gen_diff eq_thmI (isacrlsthms, isacthms);
39 val isacrlsthms''''' = ((gen_distinct eq_thmI) o (map rep_thm_G') o flat o
40 (map (thms_of_rls o #2 o #2))) (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"))
42 (* THIS IS TOO EXPENSIVE:
43 val all_ListC_thms = Global_Theory.all_thms_of (@{theory "ListC"});
44 length all_ListC_thms = 19860 <<<<<-----*)
45 val isacthys = (union Theory.eq_thy (! knowthys) (! progthys));
46 val isacthms''''' = (flat o (map Theory.axioms_of)) isacthys: (thmID * term) list;
47 val rlsthmsNOTisac''''' = gen_diff eq_thmI' (isacrlsthms''''', isacthms''''');
48 (* vvvvvvvvvvvvvv also contains all sym; ???: put ###sym_* to isacthms'''''
49 ??? ..NO: some are from isab, some from isac !!!
50 val rlsthmsNOTisac''''' =
51 [("refl", "?t = ?t"), |> map (thms_of_rls o #2 o #2) (*drop manually input id in Thm (id, thm)*)
54 |> gen_distinct Thm.eq_thm
56 |> map (apfst Thm.derivation_name) (*WN120319 returns "" after num_str, see below*)
57 |> map (apsnd prop_of); (*adapt to Theory.axioms_of below*)
59 ("o_apply", "(?f \<circ> ?g) ?x = ?f (?g ?x)"),
60 (*/------------these are not found in ListC.thy, because they are no axioms---\*)
61 ("del_base", "del [] ?x = []"),
62 ("del_rec", "del (?y # ?ys) ?x = (if ?x = ?y then ?ys else ?y # del ?ys ?x)"),
63 ("LENGTH_CONS", "LENGTH (?x # ?xs) = 1 + LENGTH ?xs"),
64 ("LENGTH_NIL", "LENGTH [] = 0"),
65 ("list_diff_def", "?a -- ?b \<equiv> foldl del ?a ?b"),
66 (*\------------these are not found in ListC.thy, because they are no axioms---/*)
67 ("take_Nil", "take ?n [] = []"),
68 ("take_Cons", "take ?n (?x # ?xs) = (case ?n of 0 \<Rightarrow> [] | Suc m \<Rightarrow> ?x # take m ?xs)"),
69 ("if_True", "(if True then ?x else ?y) = ?x"),
70 ("if_False", "(if False then ?x else ?y) = ?y"),
71 (*###*)("sym_real_mult_minus1", "- ?z1 = -1 * ?z1"),
72 ("distrib_right", "(?a + ?b) * ?c = ?a * ?c + ?b * ?c"),
73 ("distrib_left", "?a * (?b + ?c) = ?a * ?b + ?a * ?c"),
74 (*###*)(sym_realpow_twoI", "?r1 * ?r1 = ?r1 ^^^ 2"),
75 (*###*)(sym_realpow_addI", "?r1 ^^^ ?n1 * ?r1 ^^^ ?m1 = ?r1 ^^^ (?n1 + ?m1)"),
76 ("mult_1_right", "?a * 1 = ?a"),
77 (*###*)(sym_real_mult_2", "?z1 + ?z1 = 2 * ?z1"),
78 ("mult_1_left", "1 * ?a = ?a"),
79 ("mult_zero_left", "0 * ?a = 0"),
80 ("mult_zero_right", "?a * 0 = 0"),
81 ("add_0_left", "0 + ?a = ?a"),
82 ("add_0_right", "?a + 0 = ?a"),
83 ("divide_zero_left", "0 / ?a = 0"),
84 (*###*)(sym_mult_assoc", "?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1"),
85 ("order_refl", "?w \<le> ?w"),
86 ("minus_minus", "- (- ?a) = ?a"),
87 ("mult_commute", "?z * ?w = ?w * ?z"),
88 ("mult_assoc", "?z1.0 * ?z2.0 * ?z3.0 = ?z1.0 * (?z2.0 * ?z3.0)"),
89 ("add_commute", "?a + ?b = ?b + ?a"),
90 ("add_left_commute", "?b + (?a + ?c) = ?a + (?b + ?c)"),
91 ("add_assoc", "?a + ?b + ?c = ?a + (?b + ?c)"),
92 ("minus_mult_left", "- ?a1 * ?b1 = - (?a1 * ?b1)"),
93 ("right_minus", "?a + - ?a = 0"),
94 (*###*)("sym_add_assoc", "?a1 + (?b1 + ?c1) = ?a1 + ?b1 + ?c1"),
95 ("left_diff_distrib", "(?a - ?b) * ?c = ?a * ?c - ?b * ?c"),
96 ("right_diff_distrib", "?a * (?b - ?c) = ?a * ?b - ?a * ?c"),
97 ("minus_divide_left", "- ?a1 / ?b1 = - (?a1 / ?b1)"),
98 ("times_divide_eq_right", "?a * (?b / ?c) = ?a * ?b / ?c"),
99 ("times_divide_eq_left", "?b / ?c * ?a = ?b * ?a / ?c"),
100 ("divide_divide_eq_left", "?a / ?b / ?c = ?a / (?b * ?c)"),
101 ("divide_divide_eq_right", "?a / (?b / ?c) = ?a * ?c / ?b"),
102 ("divide_1", "?a / 1 = ?a"),
103 ("add_divide_distrib", "(?a + ?b) / ?c = ?a / ?c + ?b / ?c"),
104 (*###*)("sym_rmult_assoc", "?m1 * (?n1 * ?k1) = ?m1 * ?n1 * ?k1")]: (string * thm) list
107 "-------- retrieve isa-b/c theories from Isabelle -------";
108 "-------- retrieve isa-b/c theories from Isabelle -------";
109 "-------- retrieve isa-b/c theories from Isabelle -------";
110 val first_ProgLang_thy = @{theory ListC}
111 val first_Knowledge_thy = @{theory Delete} (*see WN120321.TODO rearrange theories*)
112 val allthys = (*!!! @{theory} :: ..START WITH Isac.thy..*) Theory.ancestors_of @{theory};
114 drop ((find_index (curry Theory.eq_thy first_ProgLang_thy) allthys) + 1, allthys);
116 take ((find_index (curry Theory.eq_thy first_ProgLang_thy) allthys) + 1, allthys);
118 take ((find_index (curry Theory.eq_thy first_Knowledge_thy) isacthys') + 1, isacthys');
119 val progthys' = (*WN120321.TODO rearrange theories -------vvv*)
120 drop ((find_index (curry Theory.eq_thy first_Knowledge_thy) isacthys') + 1 +3, isacthys');
122 map Context.theory_name allthys;
123 map Context.theory_name isabthys';
124 map Context.theory_name isacthys' = ["Isac", "Inverse_Z_Transform", "DiophantEq", "AlgEin",
125 "Biegelinie", "Vect", "PolyMinus", "Frontend", "Partial_Fractions", "DiffApp", "Test", "EqSystem",
126 "Integrate", "Diff", "LogExp", "Trig", "Calculus", "PolyEq", "RootRatEq", "RootRat", "RatEq",
127 "RootEq", "LinEq", "Root", "Equation", "Rational", "Poly", "Simplify", "Atools", "Descript",
128 "Delete", "xmlsrc", "Interpret", "ProgLang", "Script", "Tools", "ListC"]; (*WN120201 true*)
129 (*see WN120321.TODO rearrange theories: ATTENTION with ProgLang.thy etc*)
130 map Context.theory_name knowthys' = ["Isac", "Inverse_Z_Transform", "DiophantEq", "AlgEin",
131 "Biegelinie", "Vect", "PolyMinus", "Frontend", "Partial_Fractions", "DiffApp", "Test", "EqSystem",
132 "Integrate", "Diff", "LogExp", "Trig", "Calculus", "PolyEq", "RootRatEq", "RootRat", "RatEq",
133 "RootEq", "LinEq", "Root", "Equation", "Rational", "Poly", "Simplify", "Atools", "Descript",
134 "Delete"]; (*WN120201 true*)
135 map Context.theory_name progthys' = ["Script", "Tools", "ListC"]; (*WN120201 true*)
137 "-------- prop_of thm .. Theory.axioms_of ---------------";
138 "-------- prop_of thm .. Theory.axioms_of ---------------";
139 "-------- prop_of thm .. Theory.axioms_of ---------------";
140 val isacrlsthms''''' = (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"))
141 |> map (thms_of_rls o #2 o #2) (*drop manually input id in Thm (id, thm)*)
144 |> gen_distinct Thm.eq_thm
146 |> map (apfst Thm.derivation_name) (*WN120319 returns "" after num_str, see below*)
147 |> map (apsnd prop_of); (*adapt to Theory.axioms_of below*)
149 val isacthms''''' = (flat o (map Theory.axioms_of)) isacthys: (thmID * term) list;
150 "---------------------------------------------------------------------------------";
151 "the formats of prop_of thm .. Theory.axioms_of are too different for comparison: ";
152 "---------------------------------------------------------------------------------";
154 (*assoc (isacrlsthms''''', "Poly.realpow_oneI") = NONE; ---thus:*)
155 val one1 = num_str @{thm realpow_oneI};
156 atomty (prop_of one1);
158 *** Const (HOL.Trueprop, bool => prop)
159 *** . Const (HOL.eq, real => real => bool)
160 *** . . Const (Atools.pow, real => real => real)
161 *** . . . Var ((r, 0), real)
162 *** . . . Free (1, real)
163 *** . . Var ((r, 0), real)
165 val SOME coll2 = assoc (isacthms''''', "Poly.realpow_oneI");
168 *** Const (all, (real => prop) => prop)
169 *** . Abs (r, real,..
170 *** . . Const (HOL.Trueprop, bool => prop)
171 *** . . . Const (HOL.eq, real => real => bool)
172 *** . . . . Const (Atools.pow, real => real => real)
173 *** . . . . . Bound 0
174 *** . . . . . Const (Groups.one_class.one, real)
178 (*assoc (isacrlsthms''''', "Poly.realpow_plus_1_atom") = NONE; ---thus:*)
179 val one1 = num_str @{thm realpow_plus_1_atom};
180 atomty (prop_of one1);
182 *** Const (==>, prop => prop => prop)
183 *** . Const (HOL.Trueprop, bool => prop)
184 *** . . Const (Atools.is'_atom, real => bool)
185 *** . . . Var ((r, 0), real)
186 *** . Const (HOL.Trueprop, bool => prop)
187 *** . . Const (HOL.eq, real => real => bool)
188 *** . . . Const (Groups.times_class.times, real => real => real)
189 *** . . . . Var ((r, 0), real)
190 *** . . . . Const (Atools.pow, real => real => real)
191 *** . . . . . Var ((r, 0), real)
192 *** . . . . . Var ((n, 0), real)
193 *** . . . Const (Atools.pow, real => real => real)
194 *** . . . . Var ((r, 0), real)
195 *** . . . . Const (Groups.plus_class.plus, real => real => real)
196 *** . . . . . Free (1, real)
197 *** . . . . . Var ((n, 0), real)
199 val SOME coll2 = assoc (isacthms''''', "Poly.realpow_plus_1_atom");
202 *** Const (all, (real => prop) => prop)
203 *** . Abs (r, real,..
204 *** . . Const (all, (real => prop) => prop)
205 *** . . . Abs (n, real,..
206 *** . . . . Const (==>, prop => prop => prop)
207 *** . . . . . Const (HOL.Trueprop, bool => prop)
208 *** . . . . . . Const (Atools.is'_atom, real => bool)
209 *** . . . . . . . Bound 1
210 *** . . . . . Const (HOL.Trueprop, bool => prop)
211 *** . . . . . . Const (HOL.eq, real => real => bool)
212 *** . . . . . . . Const (Groups.times_class.times, real => real => real)
213 *** . . . . . . . . Bound 1
214 *** . . . . . . . . Const (Atools.pow, real => real => real)
215 *** . . . . . . . . . Bound 1
216 *** . . . . . . . . . Bound 0
217 *** . . . . . . . Const (Atools.pow, real => real => real)
218 *** . . . . . . . . Bound 1
219 *** . . . . . . . . Const (Groups.plus_class.plus, real => real => real)
220 *** . . . . . . . . . Const (Groups.one_class.one, real)
221 *** . . . . . . . . . Bound 0
224 "-------- compute val rlsthmsNOTisac --------------------";
225 "-------- compute val rlsthmsNOTisac --------------------";
226 "-------- compute val rlsthmsNOTisac --------------------";
227 (*WN120319: since num_str destoys derivation_name, we hardcode rlsthmsNOTisac.
229 (*DECISION.WN120201 wrt. identifiers of theorems, thmID, in building html presentation:
230 eg. Thm.derivation_name @{thm add_0} = "Groups.comm_monoid_add_class.add_0";
231 is long identifier, "add_0" is simple identifier
233 (1) simple identifiers, without points, conform with usage in TP-PL
234 (2) Thm (id, thm) in rls, id is simple id; entered manyally -- error prone
235 all this might change due to further automation
237 (a) retrieve id (and theory) from thm or axiom (avoids errors from (2))
238 (b) hold long identifiers, with points, as long as possible
239 (c) use thmID_of_derivation_name, thyID_of_derivation_name for retrieval.
241 (*WN110722 saved investigations:
242 val all_ListC_thms = PureThy.all_thms_of (@{theory "ListC"});
243 val all_Complex_Main_thms = PureThy.all_thms_of (@{theory "Complex_Main"});
244 delivers [] after 100 secs ...
245 subtract Thm.eq_thm (map #2 all_ListC_thms) (map #2 all_Complex_Main_thms);
246 ... because ListC contains no thms, but axioms only.
247 "----- so we cannot get isacthms as thm, only as term ---";
248 "----- but we can retain isacrlsthms as thm ---";
250 val isacrlsthms = (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"))
251 |> map (thms_of_rls o #2 o #2) (*drop manually input id in Thm (id, thm)*)
254 |> gen_distinct Thm.eq_thm
256 |> map (apfst Thm.derivation_name); (*WN120319 returns "" after num_str, see below*)
257 length isacrlsthms = 450; (*WN120319*)
258 (*[("HOL.refl", "?t = ?t"),
259 ("Fun.o_apply", "(?f \<circ> ?g) ?x = ?f (?g ?x)"),
260 ("", "1 < ?n \<Longrightarrow> NTH ?n (?x # ?xs) = NTH (?n + - 1) ?xs"), (*destroyed by num_str*)
261 ("", "NTH 1 (?x # ?xs) = ?x"), (*destroyed by num_str*)
262 ("ListC.append_Cons", "(?x # ?xs) @ ?ys = ?x # ?xs @ ?ys"), ...]: (string * thm) list
265 val isacthms = (flat o (map Theory.axioms_of)) isacthys: (thmID * term) list;
266 length isacthms = 517; (*WN120319, WN120201 509!?!*)
267 (*[("Inverse_Z_Transform.rule1", Const ("==>...", "prop \<Rightarrow> prop \<Rightarrow> prop") $ (Const (...) $ ...),
268 ("Inverse_Z_Transform.rule2", Const (...) $ Abs ("z...", "RealDef.real",...),
269 ...]: (thmID * term) list
272 (*WN120319: since num_str destoys derivation_name to "", we hardcode rlsthmsNOTisac:
274 val rlsthmsNOTisac = gen_diff eq_thmI (isacrlsthms, isacthms);
275 map fst rlsthmsNOTisac;
276 (*val it = ["HOL.refl", "Fun.o_apply", "", "", "ListC.del.del_base", "ListC.del.del_rec", "", "",
277 "ListC.list_diff_def", "List.take.take_Nil", ...]
279 length rlsthmsNOTisac = 46; (*WN120201*)
282 "-------- hard-coded val rlsthmsNOTisac -----------------";
283 "-------- hard-coded val rlsthmsNOTisac -----------------";
284 "-------- hardcode val rlsthmsNOTisac -------------------";
285 (*WN120319: since num_str destoys derivation_name, we hardcode rlsthmsNOTisac:
286 WN131121: at least ERROR Unknown fact "Real.order_refl"*)
288 [("HOL.refl", (prop_of o num_str) @{thm refl}),
289 ("Fun.o_apply", (prop_of o num_str) @{thm o_apply}),
290 (*/------------these are not found in ListC.thy, because they are no axioms---\*)
291 ("ListC.LENGTH.LENGTH_CONS", (prop_of o num_str) @{thm LENGTH_CONS}),
292 ("ListC.LENGTH.LENGTH_NIL", (prop_of o num_str) @{thm LENGTH_NIL}),
293 ("List.take_Nil", (prop_of o num_str) @{thm take_Nil}),
294 ("List.take_Cons", (prop_of o num_str) @{thm take_Cons}),
295 ("List.if_True", (prop_of o num_str) @{thm if_True}),
296 ("HOL.if_False", (prop_of o num_str) @{thm if_False}),
297 (*###("sym_real_mult_minus1", "- ?z1 = -1 * ?z1")*)
298 ("Rings.semiring_class.distrib_right", (prop_of o num_str) @{thm distrib_right}),
299 ("Rings.semiring_class.distrib_left", (prop_of o num_str) @{thm distrib_left}),
300 (*###("sym_realpow_twoI", "?r1 * ?r1 = ?r1 ^^^ 2")*)
301 (*###("sym_realpow_addI", "?r1 ^^^ ?n1 * ?r1 ^^^ ?m1 = ?r1 ^^^ (?n1 + ?m1)")*)
302 ("Groups.monoid_mult_class.mult_1_right", (prop_of o num_str) @{thm mult_1_right}),
303 (*("sym_real_mult_2", "?z1 + ?z1 = 2 * ?z1")*)
304 ("Groups.monoid_mult_class.mult_1_left", (prop_of o num_str) @{thm mult_1_left}),
305 ("Rings.mult_zero_class.mult_zero_left", (prop_of o num_str) @{thm mult_zero_left}),
306 ("Rings.mult_zero_class.mult_zero_right", (prop_of o num_str) @{thm mult_zero_right}),
307 ("Groups.monoid_add_class.add_0_left", (prop_of o num_str) @{thm add_0_left}),
308 ("Groups.monoid_add_class.add_0_right", (prop_of o num_str) @{thm add_0_right}),
309 ("Rings.division_ring_class.divide_zero_left", (prop_of o num_str) @{thm divide_zero_left}),
310 (*###("sym_mult_assoc", "?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1")*)
311 ("Real.order_refl", (prop_of o num_str) @{thm order_refl}),
312 ("Groups.group_add_class.minus_minus", (prop_of o num_str) @{thm minus_minus}),
313 ("Real.mult_commute", (prop_of o num_str) @{thm mult_commute }),
314 ("Real.mult_assoc", (prop_of o num_str) @{thm mult_assoc}),
315 ("Groups.ab_semigroup_add_class.add_commute", (prop_of o num_str) @{thm add_commute}),
316 ("Groups.ab_semigroup_add_class.add_left_commute", (prop_of o num_str) @{thm add_left_commute}),
317 ("Groups.semigroup_add_class.add_assoc", (prop_of o num_str) @{thm add_assoc}),
318 ("Rings.ring_class.minus_mult_left", (prop_of o num_str) @{thm minus_mult_left}),
319 ("Groups.group_add_class.right_minus", (prop_of o num_str) @{thm right_minus}),
320 (*###("sym_add_assoc", "?a1 + (?b1 + ?c1) = ?a1 + ?b1 + ?c1"),*)
321 ("Rings.ring_class.left_diff_distrib", (prop_of o num_str) @{thm left_diff_distrib}),
322 ("Rings.ring_class.right_diff_distrib", (prop_of o num_str) @{thm right_diff_distrib}),
323 ("Rings.division_ring_class.minus_divide_left", (prop_of o num_str) @{thm minus_divide_left}),
324 ("Rings.division_ring_class.times_divide_eq_right", (prop_of o num_str) @{thm times_divide_eq_right}),
325 ("Fields.field_class.times_divide_eq_left", (prop_of o num_str) @{thm times_divide_eq_left}),
326 ("Fields.field_inverse_zero_class.divide_divide_eq_left", (prop_of o num_str) @{thm divide_divide_eq_left}),
327 ("Fields.field_inverse_zero_class.divide_divide_eq_right", (prop_of o num_str) @{thm divide_divide_eq_right}),
328 ("Rings.division_ring_class.divide_1", (prop_of o num_str) @{thm divide_1}),
329 ("Rings.division_ring_class.add_divide_distrib", (prop_of o num_str) @{thm add_divide_distrib }),
330 (*###("sym_rmult_assoc", "?m1 * (?n1 * ?k1) = ?m1 * ?n1 * ?k1")*)
331 (* thms in Scripts: *)
332 ("Int.divide_minus1", (prop_of o num_str) @{thm divide_minus1}),
333 ("Groups.group_add_class.neg_equal_iff_equal", (prop_of o num_str) @{thm neg_equal_iff_equal})]
334 : (thmDeriv * term) list;
336 "-------- the_hier (! thehier) (collect_thydata ())------";
337 "-------- the_hier (! thehier) (collect_thydata ())------";
338 "-------- the_hier (! thehier) (collect_thydata ())------";
339 collect_thydata; (* = fn: unit -> (theID * thydata) list*)
340 thehier; (* = ref [Ptyp ("IsacKnowledge", [Html {guh = "thy_isac_IsacKnowledge-part", ...}],
341 [Ptyp ("Biegelinie", [Html {guh = "thy_isac_Biegelinie", ...}],
342 [Ptyp ("Theorems", [Html {guh = "thy_isac_Biegelinie-Theorems", ...}],
343 [Ptyp ("Belastung_Querkraft", [Hthm {guh = "thy_isac_B ...}],[]),
344 Ptyp ("Moment_Neigung", [Hthm {guh = "thy_isac_Biegeli...}],[]),
345 [])])])])] : thehier ref *)
346 the_hier (! thehier) (collect_thydata ());
348 *** insert: preserved ["Isabelle"]
349 *** insert: preserved ["Isabelle","HOL","Theorems","refl"]
350 *** insert: preserved ["Isabelle","Fun","Theorems","o_apply"]
351 see WN120320.TODO check-improve rlsthmsNOTisac: ------\
352 *** insert: preserved ["Isabelle","ListC","Theorems","del_base"]
353 *** insert: preserved ["Isabelle","ListC","Theorems","del_rec"]
354 *** insert: preserved ["Isabelle","ListC","Theorems","LENGTH_CONS"]
355 *** insert: preserved ["Isabelle","ListC","Theorems","LENGTH_NIL"]
356 *** insert: preserved ["Isabelle","ListC","Theorems","list_diff_def"]
357 see WN120320.TODO check-improve rlsthmsNOTisac: ------/
358 *** insert: preserved ["Isabelle","List","Theorems","take_Nil"]
359 *** insert: preserved ["Isabelle","List","Theorems","take_Cons"]
360 *** insert: preserved ["Isabelle","List","Theorems","if_True"]
361 Thm.get_name_hint @{t^^^^^^True} = "HOL.if_True";
362 *** insert: preserved ["Isabelle","HOL","Theorems","if_False"]
363 *** insert: preserved ["Isabelle","Rings","Theorems","distrib_right"]
364 *** insert: preserved ["Isabelle","Rings","Theorems","distrib_left"]
365 *** insert: preserved ["Isabelle","Groups","Theorems","mult_1_right"]
366 *** insert: preserved ["Isabelle","Groups","Theorems","mult_1_left"]
367 *** insert: preserved ["Isabelle","Rings","Theorems","mult_zero_left"]
368 *** insert: preserved ["Isabelle","Rings","Theorems","mult_zero_right"]
369 *** insert: preserved ["Isabelle","Groups","Theorems","add_0_left"]
370 *** insert: preserved ["Isabelle","Groups","Theorems","add_0_right"]
371 *** insert: preserved ["Isabelle","Rings","Theorems","divide_zero_left"]
372 *** insert: preserved ["Isabelle","RealDef","Theorems","order_refl"]
373 *** insert: preserved ["Isabelle","Groups","Theorems","minus_minus"]
374 *** insert: preserved ["Isabelle","RealDef","Theorems","mult_commute"]
375 *** insert: preserved ["Isabelle","RealDef","Theorems","mult_assoc"]
376 *** insert: preserved ["Isabelle","Groups","Theorems","add_commute"]
377 *** insert: preserved ["Isabelle","Groups","Theorems","add_left_commute"]
378 *** insert: preserved ["Isabelle","Groups","Theorems","add_assoc"]
379 *** insert: preserved ["Isabelle","Rings","Theorems","minus_mult_left"]
380 *** insert: preserved ["Isabelle","Groups","Theorems","right_minus"]
381 *** insert: preserved ["Isabelle","Rings","Theorems","left_diff_distrib"]
382 *** insert: preserved ["Isabelle","Rings","Theorems","right_diff_distrib"]
383 *** insert: preserved ["Isabelle","Rings","Theorems","minus_divide_left"]
384 *** insert: preserved ["Isabelle","Rings","Theorems","times_divide_eq_right"]
385 *** insert: preserved ["Isabelle","Fields","Theorems","times_divide_eq_left"]
386 *** insert: preserved ["Isabelle","Fields","Theorems","divide_divide_eq_left"]
387 *** insert: preserved ["Isabelle","Fields","Theorems","divide_divide_eq_right"]
388 *** insert: preserved ["Isabelle","Rings","Theorems","divide_1"]
389 *** insert: preserved ["Isabelle","Rings","Theorems","add_divide_distrib"]
390 *** insert: preserved ["Isabelle","Int","Theorems","divide_minus1"]
391 *** insert: preserved ["Isabelle","Groups","Theorems","neg_equal_iff_equal"]
392 ??? vvvvvvvvvvvvvv ------\
393 *** insert: preserved ["IsacScripts","Script","Theorems","arity_type_ID"]
394 *** insert: preserved ["IsacScripts","Script","Theorems","arity_type_arg"]
395 *** insert: preserved ["IsacScripts","Tools","Theorems","arity_type_cpy"]
396 *** insert: preserved ["IsacScripts","Tools","Theorems","arity_type_nam"]
397 *** insert: preserved ["IsacScripts","Tools","Theorems","arity_type_str"]
398 *** insert: preserved ["IsacScripts","Tools","Theorems","arity_type_una"]
399 *** insert: preserved ["IsacScripts","Tools","Theorems","arity_type_unl"]
400 *** insert: preserved ["IsacScripts","Tools","Theorems","arity_type_toreal"]
401 *** insert: preserved ["IsacScripts","Tools","Theorems","arity_type_unknow"]
402 *** insert: preserved ["IsacScripts","Tools","Theorems","arity_type_tobooll"]
403 *** insert: preserved ["IsacScripts","Tools","Theorems","arity_type_toreall"]
404 ??? vvvvvvvvvvvvvv ------/
405 *** insert: preserved ["IsacScripts","Tools","Rulesets","e_rls"]
406 *** insert: preserved ["IsacScripts","Tools","Rulesets","e_rrls"]
407 see WN120320.TODO check-improve rlsthmsNOTisac: ------\
408 *** insert: preserved ["IsacScripts","ListC","Theorems","LAST"] = ["IsacKnowledge","ListC"---\
409 *** insert: preserved ["IsacScripts","ListC","Theorems","hd_thm"]
410 *** insert: preserved ["IsacScripts","ListC","Theorems","tl_Nil"]
411 *** insert: preserved ["IsacScripts","ListC","Theorems","NTH_NIL"]
412 *** insert: preserved ["IsacScripts","ListC","Theorems","del_def"]
413 *** insert: preserved ["IsacScripts","ListC","Theorems","map_Nil"]
414 *** insert: preserved ["IsacScripts","ListC","Theorems","mem_Nil"]
415 *** insert: preserved ["IsacScripts","ListC","Theorems","rev_Nil"]
416 *** insert: preserved ["IsacScripts","ListC","Theorems","tl_Cons"]
417 *** insert: preserved ["IsacScripts","ListC","Theorems","zip_Nil"]
418 *** insert: preserved ["IsacScripts","ListC","Theorems","NTH_CONS"]
419 *** insert: preserved ["IsacScripts","ListC","Theorems","map_Cons"]
420 *** insert: preserved ["IsacScripts","ListC","Theorems","mem_Cons"]
421 *** insert: preserved ["IsacScripts","ListC","Theorems","null_Nil"]
422 *** insert: preserved ["IsacScripts","ListC","Theorems","rev_Cons"]
423 *** insert: preserved ["IsacScripts","ListC","Theorems","zip_Cons"]
424 *** insert: preserved ["IsacScripts","ListC","Theorems","foldr_Nil"]
425 *** insert: preserved ["IsacScripts","ListC","Theorems","null_Cons"]
426 *** insert: preserved ["IsacScripts","ListC","Theorems","LENGTH_def"]
427 *** insert: preserved ["IsacScripts","ListC","Theorems","append_Nil"]
428 *** insert: preserved ["IsacScripts","ListC","Theorems","concat_Nil"]
429 *** insert: preserved ["IsacScripts","ListC","Theorems","filter_Nil"]
430 *** insert: preserved ["IsacScripts","ListC","Theorems","foldr_Cons"]
431 *** insert: preserved ["IsacScripts","ListC","Theorems","append_Cons"]
432 *** insert: preserved ["IsacScripts","ListC","Theorems","butlast_Nil"]
433 *** insert: preserved ["IsacScripts","ListC","Theorems","concat_Cons"]
434 *** insert: preserved ["IsacScripts","ListC","Theorems","filter_Cons"]
435 *** insert: preserved ["IsacScripts","ListC","Theorems","remdups_Nil"]
436 *** insert: preserved ["IsacScripts","ListC","Theorems","butlast_Cons"]
437 *** insert: preserved ["IsacScripts","ListC","Theorems","distinct_Nil"]
438 *** insert: preserved ["IsacScripts","ListC","Theorems","remdups_Cons"]
439 *** insert: preserved ["IsacScripts","ListC","Theorems","distinct_Cons"]
440 *** insert: preserved ["IsacScripts","ListC","Theorems","dropWhile_Nil"]
441 *** insert: preserved ["IsacScripts","ListC","Theorems","takeWhile_Nil"]
442 *** insert: preserved ["IsacScripts","ListC","Theorems","dropWhile_Cons"]
443 *** insert: preserved ["IsacScripts","ListC","Theorems","takeWhile_Cons"]
444 *** insert: preserved ["IsacScripts","ListC","Theorems","list_diff_def_raw"] =["IsacKnowledge"---/
445 *** insert: preserved ["IsacKnowledge","Inverse_Z_Transform","Theorems","rule1"]
446 *** insert: preserved ["IsacKnowledge","Inverse_Z_Transform","Theorems","rule2"]
447 *** insert: preserved ["IsacKnowledge","Inverse_Z_Transform","Theorems","rule3"]
448 *** insert: preserved ["IsacKnowledge","Inverse_Z_Transform","Theorems","rule4"]
449 *** insert: preserved ["IsacKnowledge","Inverse_Z_Transform","Theorems","rule5"]
450 *** insert: preserved ["IsacKnowledge","Inverse_Z_Transform","Theorems","rule6"]
451 *** insert: preserved ["IsacKnowledge","Inverse_Z_Transform","Theorems","ruleYZ"]
452 *** insert: preserved ["IsacKnowledge","Inverse_Z_Transform","Theorems","ruleZY"]
453 *** insert: preserved ["IsacKnowledge","Inverse_Z_Transform","Rulesets","inverse_z"]
454 *** insert: preserved ["IsacKnowledge","DiophantEq","Theorems","int_isolate_add"]
455 *** insert: preserved ["IsacKnowledge","Biegelinie","Theorems","Moment_Neigung"]
456 *** insert: preserved ["IsacKnowledge","Biegelinie","Theorems","Neigung_Moment"]
457 *** insert: preserved ["IsacKnowledge","Biegelinie","Theorems","Moment_Querkraft"]
458 *** insert: preserved ["IsacKnowledge","Biegelinie","Theorems","Querkraft_Moment"]
459 *** insert: preserved ["IsacKnowledge","Biegelinie","Theorems","make_fun_explicit"]
460 *** insert: preserved ["IsacKnowledge","Biegelinie","Theorems","Belastung_Querkraft"]
461 *** insert: preserved ["IsacKnowledge","Biegelinie","Theorems","Querkraft_Belastung"]
462 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","x_quadrat"]
463 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","null_minus"]
464 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","subtrahiere"]
465 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","tausche_mal"]
466 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","tausche_plus"]
467 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","subtrahiere_1"]
468 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","tausche_minus"]
469 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","vor_minus_mal"]
470 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","tausche_mal_mal"]
471 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","tausche_vor_mal"]
472 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","tausche_vor_plus"]
473 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","addiere_vor_minus"]
474 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","subtrahiere_von_1"]
475 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","tausche_plus_plus"]
476 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","tausche_vor_minus"]
477 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","klammer_minus_mult"]
478 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","klammer_minus_plus"]
479 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","klammer_mult_minus"]
480 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","klammer_plus_minus"]
481 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","tausche_minus_plus"]
482 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","tausche_plus_minus"]
483 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","klammer_minus_minus"]
484 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","tausche_minus_minus"]
485 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","subtrahiere_vor_minus"]
486 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","vorzeichen_minus_weg1"]
487 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","vorzeichen_minus_weg2"]
488 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","vorzeichen_minus_weg3"]
489 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","vorzeichen_minus_weg4"]
490 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","addiere_eins_vor_minus"]
491 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","subtrahiere_x_minus_plus"]
492 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","subtrahiere_x_plus_minus"]
493 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","subtrahiere_x_minus1_plus"]
494 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","subtrahiere_x_minus_minus"]
495 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","subtrahiere_x_minus_plus1"]
496 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","subtrahiere_x_plus1_minus"]
497 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","subtrahiere_x_plus_minus1"]
498 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","subtrahiere_eins_vor_minus"]
499 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","subtrahiere_x_minus1_minus"]
500 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","subtrahiere_x_minus_minus1"]
501 *** insert: preserved ["IsacKnowledge","PolyMinus","Rulesets","ordne_alphabetisch"]
502 *** insert: preserved ["IsacKnowledge","PolyMinus","Rulesets","fasse_zusammen"]
503 *** insert: preserved ["IsacKnowledge","PolyMinus","Rulesets","verschoenere"]
504 *** insert: preserved ["IsacKnowledge","PolyMinus","Rulesets","ordne_monome"]
505 *** insert: preserved ["IsacKnowledge","PolyMinus","Rulesets","klammern_aufloesen"]
506 *** insert: preserved ["IsacKnowledge","PolyMinus","Rulesets","klammern_ausmultiplizieren"]
507 *** insert: preserved ["IsacKnowledge","Partial_Fractions","Theorems","ansatz_2nd_order"]
508 *** insert: preserved ["IsacKnowledge","Partial_Fractions","Theorems","ansatz_3rd_order"]
509 *** insert: preserved ["IsacKnowledge","Partial_Fractions","Theorems","ansatz_4th_order"]
510 *** insert: preserved ["IsacKnowledge","Partial_Fractions","Theorems","multiply_2nd_order"]
511 *** insert: preserved ["IsacKnowledge","Partial_Fractions","Theorems","multiply_3rd_order"]
512 *** insert: preserved ["IsacKnowledge","Partial_Fractions","Theorems","multiply_4th_order"]
513 *** insert: preserved ["IsacKnowledge","Partial_Fractions","Theorems","equival_trans_2nd_order"]
514 *** insert: preserved ["IsacKnowledge","Partial_Fractions","Theorems","equival_trans_3rd_order"]
515 *** insert: preserved ["IsacKnowledge","Partial_Fractions","Theorems","equival_trans_4th_order"]
516 *** insert: preserved ["IsacKnowledge","Partial_Fractions","Rulesets","ansatz_rls"]
517 *** insert: preserved ["IsacKnowledge","Partial_Fractions","Rulesets","multiply_ansatz"]
518 *** insert: preserved ["IsacKnowledge","Partial_Fractions","Rulesets","equival_trans"]
519 *** insert: preserved ["IsacKnowledge","DiffApp","Theorems","filterVar_Nil"]
520 *** insert: preserved ["IsacKnowledge","DiffApp","Theorems","filterVar_Const"]
521 *** insert: preserved ["IsacKnowledge","DiffApp","Rulesets","list_rls"]
522 *** insert: preserved ["IsacKnowledge","DiffApp","Rulesets","eval_rls"]
523 *** insert: preserved ["IsacKnowledge","Test","Theorems","radd_0"]
524 *** insert: preserved ["IsacKnowledge","Test","Theorems","rsqare"]
525 *** insert: preserved ["IsacKnowledge","Test","Theorems","exp_pow"]
526 *** insert: preserved ["IsacKnowledge","Test","Theorems","power_1"]
527 *** insert: preserved ["IsacKnowledge","Test","Theorems","rmult_0"]
528 *** insert: preserved ["IsacKnowledge","Test","Theorems","rmult_1"]
529 *** insert: preserved ["IsacKnowledge","Test","Theorems","root_ge0"]
530 *** insert: preserved ["IsacKnowledge","Test","Theorems","radd_assoc"]
531 *** insert: preserved ["IsacKnowledge","Test","Theorems","root_ge0_1"]
532 *** insert: preserved ["IsacKnowledge","Test","Theorems","root_ge0_2"]
533 *** insert: preserved ["IsacKnowledge","Test","Theorems","mult_square"]
534 *** insert: preserved ["IsacKnowledge","Test","Theorems","rcancel_den"]
535 *** insert: preserved ["IsacKnowledge","Test","Theorems","rmult_assoc"]
536 *** insert: preserved ["IsacKnowledge","Test","Theorems","radd_0_right"]
537 *** insert: preserved ["IsacKnowledge","Test","Theorems","radd_commute"]
538 *** insert: preserved ["IsacKnowledge","Test","Theorems","root_add_ge0"]
539 *** insert: preserved ["IsacKnowledge","Test","Theorems","rroot_to_lhs"]
540 *** insert: preserved ["IsacKnowledge","Test","Theorems","rcancel_const"]
541 *** insert: preserved ["IsacKnowledge","Test","Theorems","rmult_0_right"]
542 *** insert: preserved ["IsacKnowledge","Test","Theorems","rmult_1_right"]
543 *** insert: preserved ["IsacKnowledge","Test","Theorems","rmult_commute"]
544 *** insert: preserved ["IsacKnowledge","Test","Theorems","rbinom_power_2"]
545 *** insert: preserved ["IsacKnowledge","Test","Theorems","rcollect_right"]
546 *** insert: preserved ["IsacKnowledge","Test","Theorems","constant_square"]
547 *** insert: preserved ["IsacKnowledge","Test","Theorems","radd_real_const"]
548 *** insert: preserved ["IsacKnowledge","Test","Theorems","square_equality"]
549 *** insert: preserved ["IsacKnowledge","Test","Theorems","square_equation"]
550 *** insert: preserved ["IsacKnowledge","Test","Theorems","rdistr_div_right"]
551 *** insert: preserved ["IsacKnowledge","Test","Theorems","risolate_bdv_add"]
552 *** insert: preserved ["IsacKnowledge","Test","Theorems","rroot_square_inv"]
553 *** insert: preserved ["IsacKnowledge","Test","Theorems","rroot_times_root"]
554 *** insert: preserved ["IsacKnowledge","Test","Theorems","rshift_nominator"]
555 *** insert: preserved ["IsacKnowledge","Test","Theorems","rtwo_of_the_same"]
556 *** insert: preserved ["IsacKnowledge","Test","Theorems","radd_left_commute"]
557 *** insert: preserved ["IsacKnowledge","Test","Theorems","rcollect_one_left"]
558 *** insert: preserved ["IsacKnowledge","Test","Theorems","risolate_bdv_mult"]
559 *** insert: preserved ["IsacKnowledge","Test","Theorems","risolate_root_add"]
560 *** insert: preserved ["IsacKnowledge","Test","Theorems","risolate_root_div"]
561 *** insert: preserved ["IsacKnowledge","Test","Theorems","rroot_to_lhs_mult"]
562 *** insert: preserved ["IsacKnowledge","Test","Theorems","square_equality_0"]
563 *** insert: preserved ["IsacKnowledge","Test","Theorems","radd_mult_distrib2"]
564 *** insert: preserved ["IsacKnowledge","Test","Theorems","radd_real_const_eq"]
565 *** insert: preserved ["IsacKnowledge","Test","Theorems","rdistr_right_assoc"]
566 *** insert: preserved ["IsacKnowledge","Test","Theorems","risolate_root_mult"]
567 *** insert: preserved ["IsacKnowledge","Test","Theorems","rmult_left_commute"]
568 *** insert: preserved ["IsacKnowledge","Test","Theorems","rnorm_equation_add"]
569 *** insert: preserved ["IsacKnowledge","Test","Theorems","constant_mult_square"]
570 *** insert: preserved ["IsacKnowledge","Test","Theorems","rdistr_right_assoc_p"]
571 *** insert: preserved ["IsacKnowledge","Test","Theorems","square_equation_left"]
572 *** insert: preserved ["IsacKnowledge","Test","Theorems","risolate_bdv_mult_add"]
573 *** insert: preserved ["IsacKnowledge","Test","Theorems","rroot_to_lhs_add_mult"]
574 *** insert: preserved ["IsacKnowledge","Test","Theorems","square_equation_right"]
575 *** insert: preserved ["IsacKnowledge","Test","Theorems","rroot_times_root_assoc"]
576 *** insert: preserved ["IsacKnowledge","Test","Theorems","rtwo_of_the_same_assoc"]
577 *** insert: preserved ["IsacKnowledge","Test","Theorems","rcollect_one_left_assoc"]
578 *** insert: preserved ["IsacKnowledge","Test","Theorems","rroot_times_root_assoc_p"]
579 *** insert: preserved ["IsacKnowledge","Test","Theorems","rtwo_of_the_same_assoc_p"]
580 *** insert: preserved ["IsacKnowledge","Test","Theorems","rcollect_one_left_assoc_p"]
581 *** insert: preserved ["IsacKnowledge","Test","Rulesets","testerls"]
582 *** insert: preserved ["IsacKnowledge","Test","Rulesets","Test_simplify"]
583 *** insert: preserved ["IsacKnowledge","Test","Rulesets","tval_rls"]
584 *** insert: preserved ["IsacKnowledge","Test","Rulesets","isolate_root"]
585 *** insert: preserved ["IsacKnowledge","Test","Rulesets","isolate_bdv"]
586 *** insert: preserved ["IsacKnowledge","Test","Rulesets","matches"]
587 *** insert: preserved ["IsacKnowledge","Test","Rulesets","norm_equation"]
588 *** insert: preserved ["IsacKnowledge","Test","Rulesets","ac_plus_times"]
589 *** insert: preserved ["IsacKnowledge","Test","Rulesets","rearrange_assoc"]
590 *** insert: preserved ["IsacKnowledge","Test","Rulesets","make_polytest"]
591 *** insert: preserved ["IsacKnowledge","Test","Rulesets","expand_binomtest"]
592 *** insert: preserved ["IsacKnowledge","EqSystem","Theorems","separate_bdvs0"]
593 *** insert: preserved ["IsacKnowledge","EqSystem","Theorems","order_system_NxN"]
594 *** insert: preserved ["IsacKnowledge","EqSystem","Theorems","separate_bdvs_add"]
595 *** insert: preserved ["IsacKnowledge","EqSystem","Theorems","commute_0_equality"]
596 *** insert: preserved ["IsacKnowledge","EqSystem","Theorems","separate_bdvs_add1"]
597 *** insert: preserved ["IsacKnowledge","EqSystem","Theorems","separate_bdvs_add2"]
598 *** insert: preserved ["IsacKnowledge","EqSystem","Theorems","separate_bdvs_mult"]
599 *** insert: preserved ["IsacKnowledge","EqSystem","Rulesets","simplify_System_parenthesized"]
600 *** insert: preserved ["IsacKnowledge","EqSystem","Rulesets","simplify_System"]
601 *** insert: preserved ["IsacKnowledge","EqSystem","Rulesets","isolate_bdvs"]
602 *** insert: preserved ["IsacKnowledge","EqSystem","Rulesets","isolate_bdvs_4x4"]
603 *** insert: preserved ["IsacKnowledge","EqSystem","Rulesets","order_system"]
604 *** insert: preserved ["IsacKnowledge","EqSystem","Rulesets","order_add_mult_System"]
605 *** insert: preserved ["IsacKnowledge","EqSystem","Rulesets","norm_System_noadd_fractions"]
606 *** insert: preserved ["IsacKnowledge","EqSystem","Rulesets","norm_System"]
607 *** insert: preserved ["IsacKnowledge","Integrate","Theorems","integral_add"]
608 *** insert: preserved ["IsacKnowledge","Integrate","Theorems","integral_pow"]
609 *** insert: preserved ["IsacKnowledge","Integrate","Theorems","integral_var"]
610 *** insert: preserved ["IsacKnowledge","Integrate","Theorems","integral_mult"]
611 *** insert: preserved ["IsacKnowledge","Integrate","Theorems","integral_const"]
612 *** insert: preserved ["IsacKnowledge","Integrate","Rulesets","integration_rules"]
613 *** insert: preserved ["IsacKnowledge","Integrate","Rulesets","add_new_c"]
614 *** insert: preserved ["IsacKnowledge","Integrate","Rulesets","simplify_Integral"]
615 *** insert: preserved ["IsacKnowledge","Integrate","Rulesets","integration"]
616 *** insert: preserved ["IsacKnowledge","Integrate","Rulesets","separate_bdv2"]
617 *** insert: preserved ["IsacKnowledge","Integrate","Rulesets","norm_Rational_noadd_fractions"]
618 *** insert: preserved ["IsacKnowledge","Integrate","Rulesets","norm_Rational_rls_noadd_fractions"]
619 *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_ln"]
620 *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_cos"]
621 *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_dif"]
622 *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_exp"]
623 *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_pow"]
624 *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_sin"]
625 *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_sum"]
626 *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_var"]
627 *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_prod"]
628 *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_quot"]
629 *** insert: preserved ["IsacKnowledge","Diff","Theorems","frac_conv"]
630 *** insert: preserved ["IsacKnowledge","Diff","Theorems","root_conv"]
631 *** insert: preserved ["IsacKnowledge","Diff","Theorems","sqrt_conv"]
632 *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_const"]
633 *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_ln_chain"]
634 *** insert: preserved ["IsacKnowledge","Diff","Theorems","frac_sym_conv"]
635 *** insert: preserved ["IsacKnowledge","Diff","Theorems","root_sym_conv"]
636 *** insert: preserved ["IsacKnowledge","Diff","Theorems","sqrt_conv_bdv"]
637 *** insert: preserved ["IsacKnowledge","Diff","Theorems","sqrt_sym_conv"]
638 *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_cos_chain"]
639 *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_exp_chain"]
640 *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_pow_chain"]
641 *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_sin_chain"]
642 *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_prod_const"]
643 *** insert: preserved ["IsacKnowledge","Diff","Theorems","realpow_pow_bdv"]
644 *** insert: preserved ["IsacKnowledge","Diff","Theorems","sqrt_conv_bdv_n"]
645 *** insert: preserved ["IsacKnowledge","Diff","Rulesets","diff_rules"]
646 *** insert: preserved ["IsacKnowledge","Diff","Rulesets","norm_diff"]
647 *** insert: preserved ["IsacKnowledge","Diff","Rulesets","diff_conv"]
648 *** insert: preserved ["IsacKnowledge","Diff","Rulesets","diff_sym_conv"]
649 *** insert: preserved ["IsacKnowledge","Diff","Rulesets","erls"]
650 *** insert: preserved ["IsacKnowledge","LogExp","Theorems","equality_pow"]
651 *** insert: preserved ["IsacKnowledge","LogExp","Theorems","equality_power"]
652 *** insert: preserved ["IsacKnowledge","LogExp","Theorems","exp_invers_log"]
653 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d0_true"]
654 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","all_left"]
655 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d0_false"]
656 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","makex1_x"]
657 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","plus_leq"]
658 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d4_sub_u1"]
659 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","minus_leq"]
660 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_prescind1"]
661 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_prescind2"]
662 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_prescind3"]
663 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_prescind4"]
664 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","real_assoc_1"]
665 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","real_assoc_2"]
666 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","separate_bdv"]
667 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_collect_1"]
668 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_collect_2"]
669 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_collect_3"]
670 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_explicit1"]
671 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_explicit2"]
672 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_explicit3"]
673 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula1"]
674 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula2"]
675 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula3"]
676 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula4"]
677 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula5"]
678 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula6"]
679 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula7"]
680 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula8"]
681 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula9"]
682 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d1_isolate_div"]
683 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula1"]
684 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula2"]
685 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula3"]
686 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula4"]
687 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula5"]
688 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula6"]
689 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula7"]
690 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula8"]
691 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula9"]
692 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_isolate_div"]
693 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula10"]
694 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_isolate_div"]
695 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","real_minus_div"]
696 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","separate_1_bdv"]
697 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","separate_bdv_n"]
698 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_n_collect_1"]
699 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_n_collect_2"]
700 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_n_collect_3"]
701 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d1_isolate_add1"]
702 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d1_isolate_add2"]
703 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula10"]
704 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_isolate_add1"]
705 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_isolate_add2"]
706 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_isolate_add1"]
707 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_isolate_add2"]
708 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","complete_square1"]
709 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","complete_square2"]
710 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","complete_square3"]
711 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","complete_square4"]
712 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","complete_square5"]
713 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","separate_1_bdv_n"]
714 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","square_explicit1"]
715 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","square_explicit2"]
716 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula1_neg"]
717 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula2_neg"]
718 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula3_neg"]
719 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula4_neg"]
720 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula9_neg"]
721 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_sqrt_equation1"]
722 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_sqrt_equation2"]
723 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_sqrt_equation3"]
724 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_root_equation1"]
725 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_root_equation2"]
726 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula1_neg"]
727 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula2_neg"]
728 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula3_neg"]
729 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula4_neg"]
730 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula5_neg"]
731 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula6_neg"]
732 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula10_neg"]
733 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_reduce_equation1"]
734 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_reduce_equation2"]
735 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation1"]
736 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation2"]
737 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation3"]
738 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation4"]
739 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation5"]
740 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation6"]
741 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation7"]
742 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation8"]
743 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation9"]
744 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_collect_assoc1_1"]
745 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_collect_assoc1_2"]
746 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_collect_assoc1_3"]
747 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_collect_assoc2_1"]
748 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_collect_assoc2_2"]
749 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_collect_assoc2_3"]
750 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation10"]
751 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation11"]
752 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation12"]
753 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation13"]
754 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation14"]
755 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation15"]
756 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation16"]
757 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","cancel_leading_coeff1"]
758 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","cancel_leading_coeff2"]
759 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","cancel_leading_coeff3"]
760 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","cancel_leading_coeff4"]
761 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","cancel_leading_coeff5"]
762 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","cancel_leading_coeff6"]
763 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","cancel_leading_coeff7"]
764 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","cancel_leading_coeff8"]
765 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","cancel_leading_coeff9"]
766 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_sqrt_equation1_neg"]
767 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_n_collect_assoc1_1"]
768 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_n_collect_assoc1_2"]
769 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_n_collect_assoc1_3"]
770 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_n_collect_assoc2_1"]
771 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_n_collect_assoc2_2"]
772 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_n_collect_assoc2_3"]
773 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","cancel_leading_coeff10"]
774 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","cancel_leading_coeff11"]
775 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","cancel_leading_coeff12"]
776 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","cancel_leading_coeff13"]
777 *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","cancel_leading_coeff"]
778 *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","complete_square"]
779 *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","PolyEq_erls"]
780 *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","polyeq_simplify"]
781 *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","d0_polyeq_simplify"]
782 *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","d1_polyeq_simplify"]
783 *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","d2_polyeq_simplify"]
784 *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","d2_polyeq_bdv_only_simplify"]
785 *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","d2_polyeq_sq_only_simplify"]
786 *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","d2_polyeq_pqFormula_simplify"]
787 *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","d2_polyeq_abcFormula_simplify"]
788 *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","d3_polyeq_simplify"]
789 *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","d4_polyeq_simplify"]
790 *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","order_add_mult_in"]
791 *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","collect_bdv"]
792 *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","make_polynomial_in"]
793 *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","make_ratpoly_in"]
794 *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","separate_bdvs"]
795 *** insert: preserved ["IsacKnowledge","RootRatEq","Theorems","rootrat_equation_left_1"]
796 *** insert: preserved ["IsacKnowledge","RootRatEq","Theorems","rootrat_equation_left_2"]
797 *** insert: preserved ["IsacKnowledge","RootRatEq","Theorems","rootrat_equation_right_1"]
798 *** insert: preserved ["IsacKnowledge","RootRatEq","Theorems","rootrat_equation_right_2"]
799 *** insert: preserved ["IsacKnowledge","RootRatEq","Rulesets","RooRatEq_erls"]
800 *** insert: preserved ["IsacKnowledge","RootRatEq","Rulesets","rootrat_solve"]
801 *** insert: preserved ["IsacKnowledge","RootRat","Rulesets","rootrat_erls"]
802 *** insert: preserved ["IsacKnowledge","RootRat","Rulesets","calculate_RootRat"]
803 *** insert: preserved ["IsacKnowledge","RatEq","Theorems","real_rat_pow"]
804 *** insert: preserved ["IsacKnowledge","RatEq","Theorems","real_rat_mult_1"]
805 *** insert: preserved ["IsacKnowledge","RatEq","Theorems","real_rat_mult_2"]
806 *** insert: preserved ["IsacKnowledge","RatEq","Theorems","real_rat_mult_3"]
807 *** insert: preserved ["IsacKnowledge","RatEq","Theorems","rat_double_rat_1"]
808 *** insert: preserved ["IsacKnowledge","RatEq","Theorems","rat_double_rat_2"]
809 *** insert: preserved ["IsacKnowledge","RatEq","Theorems","rat_double_rat_3"]
810 *** insert: preserved ["IsacKnowledge","RatEq","Theorems","rat_mult_denominator_both"]
811 *** insert: preserved ["IsacKnowledge","RatEq","Theorems","rat_mult_denominator_left"]
812 *** insert: preserved ["IsacKnowledge","RatEq","Theorems","rat_mult_denominator_right"]
813 *** insert: preserved ["IsacKnowledge","RatEq","Rulesets","rateq_erls"]
814 *** insert: preserved ["IsacKnowledge","RatEq","Rulesets","RatEq_eliminate"]
815 *** insert: preserved ["IsacKnowledge","RatEq","Rulesets","RatEq_simplify"]
816 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","makex1_x"]
817 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","real_assoc_1"]
818 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","real_assoc_2"]
819 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_1"]
820 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_2"]
821 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_times_root_1"]
822 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_times_root_2"]
823 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_isolate_l_add1"]
824 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_isolate_l_add2"]
825 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_isolate_l_add3"]
826 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_isolate_l_add4"]
827 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_isolate_l_add5"]
828 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_isolate_l_add6"]
829 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_isolate_r_add1"]
830 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_isolate_r_add2"]
831 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_isolate_r_add3"]
832 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_isolate_r_add4"]
833 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_isolate_r_add5"]
834 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_isolate_r_add6"]
835 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_both_1"]
836 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_both_2"]
837 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_both_3"]
838 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_both_4"]
839 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_left_1"]
840 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_left_2"]
841 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_left_3"]
842 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_left_4"]
843 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_left_5"]
844 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_left_6"]
845 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_right_1"]
846 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_right_2"]
847 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_right_3"]
848 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_right_4"]
849 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_right_5"]
850 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_right_6"]
851 *** insert: preserved ["IsacKnowledge","RootEq","Rulesets","RootEq_erls"]
852 *** insert: preserved ["IsacKnowledge","RootEq","Rulesets","rooteq_srls"]
853 *** insert: preserved ["IsacKnowledge","RootEq","Rulesets","sqrt_isolate"]
854 *** insert: preserved ["IsacKnowledge","RootEq","Rulesets","l_sqrt_isolate"]
855 *** insert: preserved ["IsacKnowledge","RootEq","Rulesets","r_sqrt_isolate"]
856 *** insert: preserved ["IsacKnowledge","RootEq","Rulesets","rooteq_simplify"]
857 *** insert: preserved ["IsacKnowledge","LinEq","Theorems","all_left"]
858 *** insert: preserved ["IsacKnowledge","LinEq","Theorems","makex1_x"]
859 *** insert: preserved ["IsacKnowledge","LinEq","Theorems","real_assoc_1"]
860 *** insert: preserved ["IsacKnowledge","LinEq","Theorems","real_assoc_2"]
861 *** insert: preserved ["IsacKnowledge","LinEq","Theorems","lin_isolate_div"]
862 *** insert: preserved ["IsacKnowledge","LinEq","Theorems","lin_isolate_add1"]
863 *** insert: preserved ["IsacKnowledge","LinEq","Theorems","lin_isolate_add2"]
864 *** insert: preserved ["IsacKnowledge","LinEq","Rulesets","LinEq_erls"]
865 *** insert: preserved ["IsacKnowledge","LinEq","Rulesets","LinPoly_simplify"]
866 *** insert: preserved ["IsacKnowledge","LinEq","Rulesets","LinEq_simplify"]
867 *** insert: preserved ["IsacKnowledge","Root","Theorems","root_false"]
868 *** insert: preserved ["IsacKnowledge","Root","Theorems","realpow_mul"]
869 *** insert: preserved ["IsacKnowledge","Root","Theorems","real_diff_minus"]
870 *** insert: preserved ["IsacKnowledge","Root","Theorems","root_plus_minus"]
871 *** insert: preserved ["IsacKnowledge","Root","Theorems","real_root_negative"]
872 *** insert: preserved ["IsacKnowledge","Root","Theorems","real_root_positive"]
873 *** insert: preserved ["IsacKnowledge","Root","Theorems","real_mm_binom_times"]
874 *** insert: preserved ["IsacKnowledge","Root","Theorems","real_mp_binom_times"]
875 *** insert: preserved ["IsacKnowledge","Root","Theorems","real_pm_binom_times"]
876 *** insert: preserved ["IsacKnowledge","Root","Theorems","real_pp_binom_times"]
877 *** insert: preserved ["IsacKnowledge","Root","Theorems","real_plus_binom_pow2"]
878 *** insert: preserved ["IsacKnowledge","Root","Theorems","real_plus_binom_pow3"]
879 *** insert: preserved ["IsacKnowledge","Root","Theorems","real_minus_binom_pow2"]
880 *** insert: preserved ["IsacKnowledge","Root","Theorems","real_minus_binom_pow3"]
881 *** insert: preserved ["IsacKnowledge","Root","Theorems","real_plus_binom_times"]
882 *** insert: preserved ["IsacKnowledge","Root","Theorems","real_minus_binom_times"]
883 *** insert: preserved ["IsacKnowledge","Root","Theorems","real_plus_minus_binom1"]
884 *** insert: preserved ["IsacKnowledge","Root","Theorems","real_plus_minus_binom2"]
885 *** insert: preserved ["IsacKnowledge","Root","Rulesets","Root_erls"]
886 *** insert: preserved ["IsacKnowledge","Root","Rulesets","make_rooteq"]
887 *** insert: preserved ["IsacKnowledge","Root","Rulesets","expand_rootbinoms"]
888 *** insert: preserved ["IsacKnowledge","Equation","Rulesets","univariate_equation_prls"]
889 *** insert: preserved ["IsacKnowledge","Rational","Theorems","rat_add"]
890 *** insert: preserved ["IsacKnowledge","Rational","Theorems","rat_add1"]
891 *** insert: preserved ["IsacKnowledge","Rational","Theorems","rat_add2"]
892 *** insert: preserved ["IsacKnowledge","Rational","Theorems","rat_add3"]
893 *** insert: preserved ["IsacKnowledge","Rational","Theorems","rat_mult"]
894 *** insert: preserved ["IsacKnowledge","Rational","Theorems","add_minus"]
895 *** insert: preserved ["IsacKnowledge","Rational","Theorems","rat_mult2"]
896 *** insert: preserved ["IsacKnowledge","Rational","Theorems","rat_power"]
897 *** insert: preserved ["IsacKnowledge","Rational","Theorems","add_minus1"]
898 *** insert: preserved ["IsacKnowledge","Rational","Theorems","mult_cross"]
899 *** insert: preserved ["IsacKnowledge","Rational","Theorems","mult_cross1"]
900 *** insert: preserved ["IsacKnowledge","Rational","Theorems","mult_cross2"]
901 *** insert: preserved ["IsacKnowledge","Rational","Theorems","rat_add_assoc"]
902 *** insert: preserved ["IsacKnowledge","Rational","Theorems","rat_add1_assoc"]
903 *** insert: preserved ["IsacKnowledge","Rational","Theorems","rat_add2_assoc"]
904 *** insert: preserved ["IsacKnowledge","Rational","Theorems","rat_add3_assoc"]
905 *** insert: preserved ["IsacKnowledge","Rational","Theorems","rat_mult_poly_l"]
906 *** insert: preserved ["IsacKnowledge","Rational","Theorems","rat_mult_poly_r"]
907 *** insert: preserved ["IsacKnowledge","Rational","Theorems","real_divide_divide1"]
908 *** insert: preserved ["IsacKnowledge","Rational","Theorems","real_mult_div_cancel2"]
909 *** insert: preserved ["IsacKnowledge","Rational","Theorems","real_times_divide_num"]
910 *** insert: preserved ["IsacKnowledge","Rational","Theorems","real_divide_divide1_mg"]
911 *** insert: preserved ["IsacKnowledge","Rational","Theorems","real_times_divide_1_eq"]
912 *** insert: preserved ["IsacKnowledge","Rational","Rulesets","discard_minus"]
913 *** insert: preserved ["IsacKnowledge","Rational","Rulesets","calculate_Rational"]
914 *** insert: preserved ["IsacKnowledge","Rational","Rulesets","calc_rat_erls"]
915 *** insert: preserved ["IsacKnowledge","Rational","Rulesets","rational_erls"]
916 *** insert: preserved ["IsacKnowledge","Rational","Rulesets","cancel_p"]
917 *** insert: preserved ["IsacKnowledge","Rational","Rulesets","cancel"]
918 *** insert: preserved ["IsacKnowledge","Rational","Rulesets","add_fractions_p"]
919 *** insert: preserved ["IsacKnowledge","Rational","Rulesets","add_fractions_p_rls"]
920 *** insert: preserved ["IsacKnowledge","Rational","Rulesets","common_nominator"]
921 *** insert: preserved ["IsacKnowledge","Rational","Rulesets","powers_erls"]
922 *** insert: preserved ["IsacKnowledge","Rational","Rulesets","powers"]
923 *** insert: preserved ["IsacKnowledge","Rational","Rulesets","rat_mult_divide"]
924 *** insert: preserved ["IsacKnowledge","Rational","Rulesets","reduce_0_1_2"]
925 *** insert: preserved ["IsacKnowledge","Rational","Rulesets","rat_reduce_1"]
926 *** insert: preserved ["IsacKnowledge","Rational","Rulesets","norm_rat_erls"]
927 *** insert: preserved ["IsacKnowledge","Rational","Rulesets","norm_Rational"]
928 *** insert: preserved ["IsacKnowledge","Rational","Rulesets","norm_Rational_rls"]
929 *** insert: preserved ["IsacKnowledge","Rational","Rulesets","norm_Rational_parenthesized"]
930 *** insert: preserved ["IsacKnowledge","Rational","Rulesets","rat_mult_poly"]
931 *** insert: preserved ["IsacKnowledge","Rational","Rulesets","rat_mult_div_pow"]
932 *** insert: preserved ["IsacKnowledge","Rational","Rulesets","cancel_p_rls"]
933 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_pow"]
934 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_addI"]
935 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_oneI"]
936 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_twoI"]
937 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_multI"]
938 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_zeroI"]
939 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_diff_plus"]
940 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_plus_1"]
941 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_diff_minus"]
942 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_eq_oneI"]
943 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_num_collect"]
944 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_one_collect"]
945 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_def_atom"]
946 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_two_atom"]
947 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_mult_2_assoc"]
948 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_addI_atom"]
949 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_minus_odd"]
950 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_minus_even"]
951 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_minus_oneI"]
952 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_multI_poly"]
953 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_mm_binom_times"]
954 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_mp_binom_times"]
955 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_mult_2_assoc_l"]
956 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_mult_2_assoc_r"]
957 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_pm_binom_times"]
958 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_pp_binom_times"]
959 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_plus_1_atom"]
960 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_binom_pow2"]
961 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_binom_pow3"]
962 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_binom_pow4"]
963 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_binom_pow5"]
964 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_addI_assoc_l"]
965 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_addI_assoc_r"]
966 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_twoI_assoc_l"]
967 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_twoI_assoc_r"]
968 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_minus_binom_pow2"]
969 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_minus_binom_pow3"]
970 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_binom_times"]
971 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_minus_binom_times"]
972 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_num_collect_assoc"]
973 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_one_collect_assoc"]
974 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_binom_times1"]
975 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_binom_times2"]
976 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_minus_binom1"]
977 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_minus_binom2"]
978 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_plus_1_assoc_l"]
979 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_plus_1_assoc_r"]
980 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_minus_binom_pow2_p"]
981 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_minus_binom_pow3_p"]
982 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_plus_1_assoc_l2"]
983 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_num_collect_assoc_l"]
984 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_num_collect_assoc_r"]
985 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_one_collect_assoc_l"]
986 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_one_collect_assoc_r"]
987 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_minus_binom1_p"]
988 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_minus_binom2_p"]
989 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_binom_pow2_poly"]
990 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_binom_pow3_poly"]
991 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_binom_pow4_poly"]
992 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_binom_pow5_poly"]
993 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_add_mult_distrib_poly"]
994 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_minus_binom1_p_p"]
995 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_minus_binom2_p_p"]
996 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_add_mult_distrib2_poly"]
997 *** insert: preserved ["IsacKnowledge","Poly","Rulesets","norm_Poly"]
998 *** insert: preserved ["IsacKnowledge","Poly","Rulesets","Poly_erls"]
999 *** insert: preserved ["IsacKnowledge","Poly","Rulesets","expand"]
1000 *** insert: preserved ["IsacKnowledge","Poly","Rulesets","expand_poly"]
1001 *** insert: preserved ["IsacKnowledge","Poly","Rulesets","simplify_power"]
1002 *** insert: preserved ["IsacKnowledge","Poly","Rulesets","order_add_mult"]
1003 *** insert: preserved ["IsacKnowledge","Poly","Rulesets","collect_numerals"]
1004 *** insert: preserved ["IsacKnowledge","Poly","Rulesets","collect_numerals_"]
1005 *** insert: preserved ["IsacKnowledge","Poly","Rulesets","reduce_012"]
1006 *** insert: preserved ["IsacKnowledge","Poly","Rulesets","discard_parentheses"]
1007 *** insert: preserved ["IsacKnowledge","Poly","Rulesets","make_polynomial"]
1008 *** insert: preserved ["IsacKnowledge","Poly","Rulesets","expand_binoms"]
1009 *** insert: preserved ["IsacKnowledge","Poly","Rulesets","rev_rew_p"]
1010 *** insert: preserved ["IsacKnowledge","Poly","Rulesets","expand_poly_"]
1011 *** insert: preserved ["IsacKnowledge","Poly","Rulesets","expand_poly_rat_"]
1012 *** insert: preserved ["IsacKnowledge","Poly","Rulesets","simplify_power_"]
1013 *** insert: preserved ["IsacKnowledge","Poly","Rulesets","calc_add_mult_pow_"]
1014 *** insert: preserved ["IsacKnowledge","Poly","Rulesets","reduce_012_mult_"]
1015 *** insert: preserved ["IsacKnowledge","Poly","Rulesets","reduce_012_"]
1016 *** insert: preserved ["IsacKnowledge","Poly","Rulesets","discard_parentheses1"]
1017 *** insert: preserved ["IsacKnowledge","Poly","Rulesets","order_mult_rls_"]
1018 *** insert: preserved ["IsacKnowledge","Poly","Rulesets","order_add_rls_"]
1019 *** insert: preserved ["IsacKnowledge","Poly","Rulesets","make_rat_poly_with_parentheses"]
1020 *** insert: preserved ["IsacKnowledge","Atools","Theorems","or_true"]
1021 *** insert: preserved ["IsacKnowledge","Atools","Theorems","and_true"]
1022 *** insert: preserved ["IsacKnowledge","Atools","Theorems","not_true"]
1023 *** insert: preserved ["IsacKnowledge","Atools","Theorems","or_false"]
1024 *** insert: preserved ["IsacKnowledge","Atools","Theorems","rat_leq1"]
1025 *** insert: preserved ["IsacKnowledge","Atools","Theorems","rat_leq2"]
1026 *** insert: preserved ["IsacKnowledge","Atools","Theorems","rat_leq3"]
1027 *** insert: preserved ["IsacKnowledge","Atools","Theorems","rle_refl"]
1028 *** insert: preserved ["IsacKnowledge","Atools","Theorems","and_false"]
1029 *** insert: preserved ["IsacKnowledge","Atools","Theorems","last_thmI"]
1030 *** insert: preserved ["IsacKnowledge","Atools","Theorems","not_false"]
1031 *** insert: preserved ["IsacKnowledge","Atools","Theorems","or_commute"]
1032 *** insert: preserved ["IsacKnowledge","Atools","Theorems","and_commute"]
1033 *** insert: preserved ["IsacKnowledge","Atools","Theorems","real_unari_minus"]
1034 *** insert: preserved ["IsacKnowledge","Atools","Theorems","radd_left_cancel_le"]
1035 *** insert: preserved ["IsacKnowledge","Delete","Theorems","real_diff_0"]
1036 *** insert: preserved ["IsacKnowledge","Delete","Theorems","real_mult_2"]
1037 *** insert: preserved ["IsacKnowledge","Delete","Theorems","real_mult_minus1"]
1038 *** insert: preserved ["IsacKnowledge","Delete","Theorems","real_mult_left_commute"]
1039 *** insert: preserved ["IsacKnowledge","Script","Theorems","arity_type_ID"]
1040 *** insert: preserved ["IsacKnowledge","Script","Theorems","arity_type_arg"]
1041 *** insert: preserved ["IsacKnowledge","Tools","Theorems","arity_type_cpy"]
1042 *** insert: preserved ["IsacKnowledge","Tools","Theorems","arity_type_nam"]
1043 *** insert: preserved ["IsacKnowledge","Tools","Theorems","arity_type_str"]
1044 *** insert: preserved ["IsacKnowledge","Tools","Theorems","arity_type_una"]
1045 *** insert: preserved ["IsacKnowledge","Tools","Theorems","arity_type_unl"]
1046 *** insert: preserved ["IsacKnowledge","Tools","Theorems","arity_type_toreal"]
1047 *** insert: preserved ["IsacKnowledge","Tools","Theorems","arity_type_unknow"]
1048 *** insert: preserved ["IsacKnowledge","Tools","Theorems","arity_type_tobooll"]
1049 *** insert: preserved ["IsacKnowledge","Tools","Theorems","arity_type_toreall"]
1050 *** insert: preserved ["IsacKnowledge","Tools","Rulesets","e_rls"]
1051 *** insert: preserved ["IsacKnowledge","Tools","Rulesets","e_rrls"]
1052 *** insert: preserved ["IsacKnowledge","ListC","Theorems","LAST"] = ["IsacScripts","ListC"---\
1053 *** insert: preserved ["IsacKnowledge","ListC","Theorems","hd_thm"]
1054 *** insert: preserved ["IsacKnowledge","ListC","Theorems","tl_Nil"]
1055 *** insert: preserved ["IsacKnowledge","ListC","Theorems","NTH_NIL"]
1056 *** insert: preserved ["IsacKnowledge","ListC","Theorems","del_def"]
1057 *** insert: preserved ["IsacKnowledge","ListC","Theorems","map_Nil"]
1058 *** insert: preserved ["IsacKnowledge","ListC","Theorems","mem_Nil"]
1059 *** insert: preserved ["IsacKnowledge","ListC","Theorems","rev_Nil"]
1060 *** insert: preserved ["IsacKnowledge","ListC","Theorems","tl_Cons"]
1061 *** insert: preserved ["IsacKnowledge","ListC","Theorems","zip_Nil"]
1062 *** insert: preserved ["IsacKnowledge","ListC","Theorems","NTH_CONS"]
1063 *** insert: preserved ["IsacKnowledge","ListC","Theorems","map_Cons"]
1064 *** insert: preserved ["IsacKnowledge","ListC","Theorems","mem_Cons"]
1065 *** insert: preserved ["IsacKnowledge","ListC","Theorems","null_Nil"]
1066 *** insert: preserved ["IsacKnowledge","ListC","Theorems","rev_Cons"]
1067 *** insert: preserved ["IsacKnowledge","ListC","Theorems","zip_Cons"]
1068 *** insert: preserved ["IsacKnowledge","ListC","Theorems","foldr_Nil"]
1069 *** insert: preserved ["IsacKnowledge","ListC","Theorems","null_Cons"]
1070 *** insert: preserved ["IsacKnowledge","ListC","Theorems","LENGTH_def"]
1071 *** insert: preserved ["IsacKnowledge","ListC","Theorems","append_Nil"]
1072 *** insert: preserved ["IsacKnowledge","ListC","Theorems","concat_Nil"]
1073 *** insert: preserved ["IsacKnowledge","ListC","Theorems","filter_Nil"]
1074 *** insert: preserved ["IsacKnowledge","ListC","Theorems","foldr_Cons"]
1075 *** insert: preserved ["IsacKnowledge","ListC","Theorems","append_Cons"]
1076 *** insert: preserved ["IsacKnowledge","ListC","Theorems","butlast_Nil"]
1077 *** insert: preserved ["IsacKnowledge","ListC","Theorems","concat_Cons"]
1078 *** insert: preserved ["IsacKnowledge","ListC","Theorems","filter_Cons"]
1079 *** insert: preserved ["IsacKnowledge","ListC","Theorems","remdups_Nil"]
1080 *** insert: preserved ["IsacKnowledge","ListC","Theorems","butlast_Cons"]
1081 *** insert: preserved ["IsacKnowledge","ListC","Theorems","distinct_Nil"]
1082 *** insert: preserved ["IsacKnowledge","ListC","Theorems","remdups_Cons"]
1083 *** insert: preserved ["IsacKnowledge","ListC","Theorems","distinct_Cons"]
1084 *** insert: preserved ["IsacKnowledge","ListC","Theorems","dropWhile_Nil"]
1085 *** insert: preserved ["IsacKnowledge","ListC","Theorems","takeWhile_Nil"]
1086 *** insert: preserved ["IsacKnowledge","ListC","Theorems","dropWhile_Cons"]
1087 *** insert: preserved ["IsacKnowledge","ListC","Theorems","takeWhile_Cons"]
1088 *** insert: preserved ["IsacKnowledge","ListC","Theorems","list_diff_def_raw"]=["IsacScripts"---/
1093 "-------- retrieve errpats ------------------------------";
1094 "-------- retrieve errpats ------------------------------";
1095 "-------- retrieve errpats ------------------------------";
1096 val {errpats, nrls, scr = Prog prog, ...} = get_met ["diff", "differentiate_on_R"];
1097 case errpats of [("chain-rule-diff-both", _, _)] => ()
1098 | _ => error "errpats chain-rule-diff-both changed"