wneuper/isa: test/Tools/isac/Knowledge/build

     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

     7 *)

     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 --------";

    27 (* WN1204xx:

    28    view src/Pure/isac/IsacKnowledge/Isac.ML @ 37874:331e38464ada

    29    date 	Thu Jul 22 10:45:18 2010 +0200

    31 local

    32     val isacrlsthms = ((gen_distinct eq_thmI) o (map rep_thm_G') o flat o

    33 		       (map (thms_of_rls o #2 o #2))) (!ruleset');

    34     val isacthms = (flat o (map (thms_of o #2))) (!theory');

    35 in

    36     val rlsthmsNOTisac = gen_diff eq_thmI (isacrlsthms, isacthms);

    37 end;

    38 *)

    39     val isacrlsthms''''' = ((gen_distinct eq_thmI) o (map rep_thm_G') o flat o

    40 		       (map (thms_of_rls o #2 o #2))) (!ruleset'):  (thmID * thm) list;

    41 (* THIS IS TOO EXPENSIVE:

    42 val all_ListC_thms = Global_Theory.all_thms_of (@{theory "ListC"});

    43 length all_ListC_thms = 19860 <<<<<-----*)

    44 val isacthys = (union Theory.eq_thy (! knowthys) (! progthys));

    45   val isacthms''''' = (flat o (map Theory.axioms_of)) isacthys: (thmID * term) list;

    46     val rlsthmsNOTisac''''' = gen_diff eq_thmI' (isacrlsthms''''', isacthms''''');

    47 (*  vvvvvvvvvvvvvv also contains all sym; ???: put ###sym_* to isacthms'''''

    48                                           ??? ..NO: some are from isab, some from isac !!!

    49 val rlsthmsNOTisac''''' =

    50    [("refl", "?t = ?t"),   |> map (thms_of_rls o #2 o #2) (*drop manually input id in Thm (id, thm)*)

    51   |> flat

    52   |> map thm_of_thm

    53   |> gen_distinct Thm.eq_thm

    54   |> map (` I)

    55   |> map (apfst Thm.derivation_name) (*WN120319 returns "" after num_str, see below*)

    56   |> map (apsnd prop_of);            (*adapt to Theory.axioms_of below*)

    58     ("o_apply", "(?f \<circ> ?g) ?x = ?f (?g ?x)"),

    59     (*/------------these are not found in ListC.thy, because they are no axioms---\*)

    60     ("del_base", "del [] ?x = []"),

    61     ("del_rec", "del (?y # ?ys) ?x = (if ?x = ?y then ?ys else ?y # del ?ys ?x)"),

    62     ("LENGTH_CONS", "LENGTH (?x # ?xs) = 1 + LENGTH ?xs"),

    63     ("LENGTH_NIL", "LENGTH [] = 0"),

    64     ("list_diff_def", "?a -- ?b \<equiv> foldl del ?a ?b"),

    65     (*\------------these are not found in ListC.thy, because they are no axioms---/*)

    66     ("take_Nil", "take ?n [] = []"),

    67     ("take_Cons", "take ?n (?x # ?xs) = (case ?n of 0 \<Rightarrow> [] | Suc m \<Rightarrow> ?x # take m ?xs)"),

    68     ("if_True", "(if True then ?x else ?y) = ?x"),

    69     ("if_False", "(if False then ?x else ?y) = ?y"),

    70     (*###*)("sym_real_mult_minus1", "- ?z1 = -1 * ?z1"),

    71     ("distrib_right", "(?a + ?b) * ?c = ?a * ?c + ?b * ?c"),

    72     ("distrib_left", "?a * (?b + ?c) = ?a * ?b + ?a * ?c"),

    73     (*###*)(sym_realpow_twoI", "?r1 * ?r1 = ?r1 ^^^ 2"),

    74     (*###*)(sym_realpow_addI", "?r1 ^^^ ?n1 * ?r1 ^^^ ?m1 = ?r1 ^^^ (?n1 + ?m1)"),

    75     ("mult_1_right", "?a * 1 = ?a"),

    76     (*###*)(sym_real_mult_2", "?z1 + ?z1 = 2 * ?z1"),

    77     ("mult_1_left", "1 * ?a = ?a"),

    78     ("mult_zero_left", "0 * ?a = 0"),

    79     ("mult_zero_right", "?a * 0 = 0"),

    80     ("add_0_left", "0 + ?a = ?a"),

    81     ("add_0_right", "?a + 0 = ?a"),

    82     ("divide_zero_left", "0 / ?a = 0"),

    83     (*###*)(sym_mult_assoc", "?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1"),

    84     ("order_refl", "?w \<le> ?w"),

    85     ("minus_minus", "- (- ?a) = ?a"),

    86     ("mult_commute", "?z * ?w = ?w * ?z"),

    87     ("mult_assoc", "?z1.0 * ?z2.0 * ?z3.0 = ?z1.0 * (?z2.0 * ?z3.0)"),

    88     ("add_commute", "?a + ?b = ?b + ?a"),

    89     ("add_left_commute", "?b + (?a + ?c) = ?a + (?b + ?c)"),

    90     ("add_assoc", "?a + ?b + ?c = ?a + (?b + ?c)"),

    91     ("minus_mult_left", "- ?a1 * ?b1 = - (?a1 * ?b1)"),

    92     ("right_minus", "?a + - ?a = 0"),

    93     (*###*)("sym_add_assoc", "?a1 + (?b1 + ?c1) = ?a1 + ?b1 + ?c1"),

    94     ("left_diff_distrib", "(?a - ?b) * ?c = ?a * ?c - ?b * ?c"),

    95     ("right_diff_distrib", "?a * (?b - ?c) = ?a * ?b - ?a * ?c"),

    96     ("minus_divide_left", "- ?a1 / ?b1 = - (?a1 / ?b1)"),

    97     ("times_divide_eq_right", "?a * (?b / ?c) = ?a * ?b / ?c"),

    98     ("times_divide_eq_left", "?b / ?c * ?a = ?b * ?a / ?c"),

    99     ("divide_divide_eq_left", "?a / ?b / ?c = ?a / (?b * ?c)"),

   100     ("divide_divide_eq_right", "?a / (?b / ?c) = ?a * ?c / ?b"),

   101     ("divide_1", "?a / 1 = ?a"),

   102     ("add_divide_distrib", "(?a + ?b) / ?c = ?a / ?c + ?b / ?c"),

   103     (*###*)("sym_rmult_assoc", "?m1 * (?n1 * ?k1) = ?m1 * ?n1 * ?k1")]: (string * thm) list

   104 *)

   106 "-------- retrieve isa-b/c theories from Isabelle -------";

   107 "-------- retrieve isa-b/c theories from Isabelle -------";

   108 "-------- retrieve isa-b/c theories from Isabelle -------";

   109   val first_ProgLang_thy = @{theory ListC}

   110   val first_Knowledge_thy = @{theory Delete}  (*see WN120321.TODO rearrange theories*)

   111   val allthys = (*!!! @{theory} :: ..START WITH Isac.thy..*) Theory.ancestors_of @{theory};

   112   val isabthys' =

   113     drop ((find_index (curry Theory.eq_thy first_ProgLang_thy) allthys) + 1, allthys);

   114   val isacthys' =

   115     take ((find_index (curry Theory.eq_thy first_ProgLang_thy) allthys) + 1, allthys);

   116   val knowthys' =

   117     take ((find_index (curry Theory.eq_thy first_Knowledge_thy) isacthys') + 1, isacthys');

   118   val progthys' =                   (*WN120321.TODO rearrange theories -------vvv*)

   119     drop ((find_index (curry Theory.eq_thy first_Knowledge_thy) isacthys') + 1 +3, isacthys');

   121 map Context.theory_name allthys;

   122 map Context.theory_name isabthys';

   123 map Context.theory_name isacthys' = ["Isac", "Inverse_Z_Transform", "DiophantEq", "AlgEin",

   124   "Biegelinie", "Vect", "PolyMinus", "Frontend", "Partial_Fractions", "DiffApp", "Test", "EqSystem",

   125   "Integrate", "Diff", "LogExp", "Trig", "Calculus", "PolyEq", "RootRatEq", "RootRat", "RatEq",

   126   "RootEq", "LinEq", "Root", "Equation", "Rational", "Poly", "Simplify", "Atools", "Descript",

   127   "Delete", "xmlsrc", "Interpret", "ProgLang", "Script", "Tools", "ListC"];  (*WN120201 true*)

   128 (*see WN120321.TODO rearrange theories: ATTENTION with ProgLang.thy etc*)

   129 map Context.theory_name knowthys' = ["Isac", "Inverse_Z_Transform", "DiophantEq", "AlgEin",

   130   "Biegelinie", "Vect", "PolyMinus", "Frontend", "Partial_Fractions", "DiffApp", "Test", "EqSystem",

   131   "Integrate", "Diff", "LogExp", "Trig", "Calculus", "PolyEq", "RootRatEq", "RootRat", "RatEq",

   132   "RootEq", "LinEq", "Root", "Equation", "Rational", "Poly", "Simplify", "Atools", "Descript",

   133   "Delete"];  (*WN120201 true*)

   134 map Context.theory_name progthys' = ["Script", "Tools", "ListC"];  (*WN120201 true*)

   136 "-------- prop_of thm .. Theory.axioms_of ---------------";

   137 "-------- prop_of thm .. Theory.axioms_of ---------------";

   138 "-------- prop_of thm .. Theory.axioms_of ---------------";

   139 val isacrlsthms''''' = ! ruleset'

   140   |> map (thms_of_rls o #2 o #2) (*drop manually input id in Thm (id, thm)*)

   141   |> flat

   142   |> map thm_of_thm

   143   |> gen_distinct Thm.eq_thm

   144   |> map (` I)

   145   |> map (apfst Thm.derivation_name) (*WN120319 returns "" after num_str, see below*)

   146   |> map (apsnd prop_of);            (*adapt to Theory.axioms_of below*)

   148 val isacthms''''' = (flat o (map Theory.axioms_of)) isacthys: (thmID * term) list;

   149 "---------------------------------------------------------------------------------";

   150 "the formats of prop_of thm .. Theory.axioms_of are too different for comparison: ";

   151 "---------------------------------------------------------------------------------";

   153 (*assoc (isacrlsthms''''', "Poly.realpow_oneI") = NONE; ---thus:*)

   154 val one1 = num_str @{thm realpow_oneI};

   155 atomty (prop_of one1);

   156 (****

   157 *** Const (HOL.Trueprop, bool => prop)

   158 *** . Const (HOL.eq, real => real => bool)

   159 *** . . Const (Atools.pow, real => real => real)

   160 *** . . . Var ((r, 0), real)

   161 *** . . . Free (1, real)

   162 *** . . Var ((r, 0), real)

   163 *** *)

   164 val SOME coll2 = assoc (isacthms''''', "Poly.realpow_oneI");

   165 atomty coll2;

   166 (****

   167 *** Const (all, (real => prop) => prop)

   168 *** . Abs (r, real,..

   169 *** . . Const (HOL.Trueprop, bool => prop)

   170 *** . . . Const (HOL.eq, real => real => bool)

   171 *** . . . . Const (Atools.pow, real => real => real)

   172 *** . . . . . Bound 0

   173 *** . . . . . Const (Groups.one_class.one, real)

   174 *** . . . . Bound 0

   175 ***  *)

   177 (*assoc (isacrlsthms''''', "Poly.realpow_plus_1_atom") = NONE; ---thus:*)

   178 val one1 = num_str @{thm realpow_plus_1_atom};

   179 atomty (prop_of one1);

   180 (****

   181 *** Const (==>, prop => prop => prop)

   182 *** . Const (HOL.Trueprop, bool => prop)

   183 *** . . Const (Atools.is'_atom, real => bool)

   184 *** . . . Var ((r, 0), real)

   185 *** . Const (HOL.Trueprop, bool => prop)

   186 *** . . Const (HOL.eq, real => real => bool)

   187 *** . . . Const (Groups.times_class.times, real => real => real)

   188 *** . . . . Var ((r, 0), real)

   189 *** . . . . Const (Atools.pow, real => real => real)

   190 *** . . . . . Var ((r, 0), real)

   191 *** . . . . . Var ((n, 0), real)

   192 *** . . . Const (Atools.pow, real => real => real)

   193 *** . . . . Var ((r, 0), real)

   194 *** . . . . Const (Groups.plus_class.plus, real => real => real)

   195 *** . . . . . Free (1, real)

   196 *** . . . . . Var ((n, 0), real)

   197 *** *)

   198 val SOME coll2 = assoc (isacthms''''', "Poly.realpow_plus_1_atom");

   199 atomty coll2;

   200 (****

   201 *** Const (all, (real => prop) => prop)

   202 *** . Abs (r, real,..

   203 *** . . Const (all, (real => prop) => prop)

   204 *** . . . Abs (n, real,..

   205 *** . . . . Const (==>, prop => prop => prop)

   206 *** . . . . . Const (HOL.Trueprop, bool => prop)

   207 *** . . . . . . Const (Atools.is'_atom, real => bool)

   208 *** . . . . . . . Bound 1

   209 *** . . . . . Const (HOL.Trueprop, bool => prop)

   210 *** . . . . . . Const (HOL.eq, real => real => bool)

   211 *** . . . . . . . Const (Groups.times_class.times, real => real => real)

   212 *** . . . . . . . . Bound 1

   213 *** . . . . . . . . Const (Atools.pow, real => real => real)

   214 *** . . . . . . . . . Bound 1

   215 *** . . . . . . . . . Bound 0

   216 *** . . . . . . . Const (Atools.pow, real => real => real)

   217 *** . . . . . . . . Bound 1

   218 *** . . . . . . . . Const (Groups.plus_class.plus, real => real => real)

   219 *** . . . . . . . . . Const (Groups.one_class.one, real)

   220 *** . . . . . . . . . Bound 0

   221 *** *)

   223 "-------- compute val rlsthmsNOTisac --------------------";

   224 "-------- compute val rlsthmsNOTisac --------------------";

   225 "-------- compute val rlsthmsNOTisac --------------------";

   226 (*WN120319: since num_str destoys derivation_name, we hardcode rlsthmsNOTisac.

   227 *)

   228 (*DECISION.WN120201 wrt. identifiers of theorems, thmID, in building html presentation:

   229   eg. Thm.derivation_name @{thm add_0} = "Groups.comm_monoid_add_class.add_0";

   230   is long identifier, "add_0" is simple identifier

   231   given:

   232   (1) simple identifiers, without points, conform with usage in TP-PL

   233   (2) Thm (id, thm) in rls, id is simple id; entered manyally -- error prone

   234         all this might change due to further automation

   235   thus decision

   236   (a) retrieve id (and theory) from thm or axiom (avoids errors from (2))

   237   (b) hold long identifiers, with points, as long as possible

   238   (c) use thmID_of_derivation_name, thyID_of_derivation_name for retrieval.

   239 *)

   240 (*WN110722 saved investigations:

   241 val all_ListC_thms = PureThy.all_thms_of (@{theory "ListC"});

   242 val all_Complex_Main_thms = PureThy.all_thms_of (@{theory "Complex_Main"});

   243    delivers [] after 100 secs ...

   244 subtract Thm.eq_thm (map #2 all_ListC_thms) (map #2 all_Complex_Main_thms);

   245 ... because ListC contains no thms, but axioms only.

   246 "----- so we cannot get isacthms as thm, only as term ---";

   247 "----- but we can retain isacrlsthms as thm ---";

   248 *)

   249 val isacrlsthms = ! ruleset'

   250   |> map (thms_of_rls o #2 o #2) (*drop manually input id in Thm (id, thm)*)

   251   |> flat

   252   |> map thm_of_thm

   253   |> gen_distinct Thm.eq_thm

   254   |> map (` I)

   255   |> map (apfst Thm.derivation_name); (*WN120319 returns "" after num_str, see below*)

   256 length isacrlsthms = 450; (*WN120319*)

   257 (*[("HOL.refl", "?t = ?t"),

   258    ("Fun.o_apply", "(?f \<circ> ?g) ?x = ?f (?g ?x)"),

   259    ("", "1 < ?n \<Longrightarrow> NTH ?n (?x # ?xs) = NTH (?n + - 1) ?xs"), (*destroyed by num_str*)

   260    ("", "NTH 1 (?x # ?xs) = ?x"),                             (*destroyed by num_str*)

   261    ("ListC.append_Cons", "(?x # ?xs) @ ?ys = ?x # ?xs @ ?ys"), ...]: (string * thm) list

   262 *)

   264 val isacthms = (flat o (map Theory.axioms_of)) isacthys: (thmID * term) list;

   265 length isacthms = 517; (*WN120319, WN120201 509!?!*)

   266 (*[("Inverse_Z_Transform.rule1", Const ("==>...", "prop \<Rightarrow> prop \<Rightarrow> prop") $ (Const (...) $ ...),

   267    ("Inverse_Z_Transform.rule2", Const (...) $ Abs ("z...", "RealDef.real",...),

   268    ...]: (thmID * term) list

   269 *)

   271 (*WN120319: since num_str destoys derivation_name to "", we hardcode rlsthmsNOTisac:

   273 val rlsthmsNOTisac = gen_diff eq_thmI (isacrlsthms, isacthms);

   274 map fst rlsthmsNOTisac;

   275 (*val it = ["HOL.refl", "Fun.o_apply", "", "", "ListC.del.del_base", "ListC.del.del_rec", "", "",

   276   "ListC.list_diff_def", "List.take.take_Nil", ...]

   277 *)

   278 length rlsthmsNOTisac = 46; (*WN120201*)

   279 *)

   281 "-------- hard-coded val rlsthmsNOTisac -----------------";

   282 "-------- hard-coded val rlsthmsNOTisac -----------------";

   283 "-------- hardcode val rlsthmsNOTisac -------------------";

   284 (*WN120319: since num_str destoys derivation_name, we hardcode rlsthmsNOTisac:*)

   285 val rlsthmsNOTisac =

   286  [("HOL.refl", (prop_of o num_str) @{thm refl}),

   287   ("Fun.o_apply", (prop_of o num_str) @{thm o_apply}),

   288   (*/------------these are not found in ListC.thy, because they are no axioms---\*)

   289   ("ListC.del.del_base", (prop_of o num_str) @{thm del_base}),

   290   ("ListC.del.del_rec", (prop_of o num_str) @{thm del_rec}),

   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   ("ListC.list_diff_def", (prop_of o num_str) @{thm list_diff_def}),

   294   (*\------------these are not found in ListC.thy, because they are no axioms---/*)

   295   ("List.take_Nil", (prop_of o num_str) @{thm take_Nil}),

   296   ("List.take_Cons", (prop_of o num_str) @{thm take_Cons}),

   297   ("List.if_True", (prop_of o num_str) @{thm if_True}),

   298   ("HOL.if_False", (prop_of o num_str) @{thm if_False}),

   299   (*###("sym_real_mult_minus1", "- ?z1 = -1 * ?z1")*)

   300   ("Rings.semiring_class.distrib_right", (prop_of o num_str) @{thm distrib_right}),

   301   ("Rings.semiring_class.distrib_left", (prop_of o num_str) @{thm distrib_left}),

   302   (*###("sym_realpow_twoI", "?r1 * ?r1 = ?r1 ^^^ 2")*)

   303   (*###("sym_realpow_addI", "?r1 ^^^ ?n1 * ?r1 ^^^ ?m1 = ?r1 ^^^ (?n1 + ?m1)")*)

   304   ("Groups.monoid_mult_class.mult_1_right", (prop_of o num_str) @{thm mult_1_right}),

   305   (*("sym_real_mult_2", "?z1 + ?z1 = 2 * ?z1")*)

   306   ("Groups.monoid_mult_class.mult_1_left", (prop_of o num_str) @{thm mult_1_left}),

   307   ("Rings.mult_zero_class.mult_zero_left", (prop_of o num_str) @{thm mult_zero_left}),

   308   ("Rings.mult_zero_class.mult_zero_right", (prop_of o num_str) @{thm mult_zero_right}),

   309   ("Groups.monoid_add_class.add_0_left", (prop_of o num_str) @{thm add_0_left}),

   310   ("Groups.monoid_add_class.add_0_right", (prop_of o num_str) @{thm add_0_right}),

   311   ("Rings.division_ring_class.divide_zero_left", (prop_of o num_str) @{thm divide_zero_left}),

   312   (*###("sym_mult_assoc", "?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1")*)

   313   ("RealDef.order_refl", (prop_of o num_str) @{thm order_refl}),

   314   ("Groups.group_add_class.minus_minus", (prop_of o num_str) @{thm minus_minus}),

   315   ("RealDef.mult_commute", (prop_of o num_str) @{thm mult_commute }),

   316   ("RealDef.mult_assoc", (prop_of o num_str) @{thm mult_assoc}),

   317   ("Groups.ab_semigroup_add_class.add_commute", (prop_of o num_str) @{thm add_commute}),

   318   ("Groups.ab_semigroup_add_class.add_left_commute", (prop_of o num_str) @{thm add_left_commute}),

   319   ("Groups.semigroup_add_class.add_assoc", (prop_of o num_str) @{thm add_assoc}),

   320   ("Rings.ring_class.minus_mult_left", (prop_of o num_str) @{thm minus_mult_left}),

   321   ("Groups.group_add_class.right_minus", (prop_of o num_str) @{thm right_minus}),

   322   (*###("sym_add_assoc", "?a1 + (?b1 + ?c1) = ?a1 + ?b1 + ?c1"),*)

   323   ("Rings.ring_class.left_diff_distrib", (prop_of o num_str) @{thm left_diff_distrib}),

   324   ("Rings.ring_class.right_diff_distrib", (prop_of o num_str) @{thm right_diff_distrib}),

   325   ("Rings.division_ring_class.minus_divide_left", (prop_of o num_str) @{thm minus_divide_left}),

   326   ("Rings.division_ring_class.times_divide_eq_right", (prop_of o num_str) @{thm times_divide_eq_right}),

   327   ("Fields.field_class.times_divide_eq_left", (prop_of o num_str) @{thm times_divide_eq_left}),

   328   ("Fields.field_inverse_zero_class.divide_divide_eq_left", (prop_of o num_str) @{thm divide_divide_eq_left}),

   329   ("Fields.field_inverse_zero_class.divide_divide_eq_right", (prop_of o num_str) @{thm divide_divide_eq_right}),

   330   ("Rings.division_ring_class.divide_1", (prop_of o num_str) @{thm divide_1}),

   331   ("Rings.division_ring_class.add_divide_distrib", (prop_of o num_str) @{thm add_divide_distrib }),

   332   (*###("sym_rmult_assoc", "?m1 * (?n1 * ?k1) = ?m1 * ?n1 * ?k1")*)

   333   (* thms in Scripts: *)

   334   ("Int.divide_minus1", (prop_of o num_str) @{thm divide_minus1}),

   335   ("Groups.group_add_class.neg_equal_iff_equal", (prop_of o num_str) @{thm neg_equal_iff_equal})]

   336   : (thmDeriv * term) list;

   338 "-------- the_hier (! thehier) (collect_thydata ())------";

   339 "-------- the_hier (! thehier) (collect_thydata ())------";

   340 "-------- the_hier (! thehier) (collect_thydata ())------";

   341 collect_thydata; (* = fn: unit -> (theID * thydata) list*)

   342 thehier; (* = ref [Ptyp ("IsacKnowledge", [Html {guh = "thy_isac_IsacKnowledge-part", ...}],

   343                     [Ptyp ("Biegelinie", [Html {guh = "thy_isac_Biegelinie", ...}],

   344                       [Ptyp ("Theorems", [Html {guh = "thy_isac_Biegelinie-Theorems", ...}],

   345                         [Ptyp ("Belastung_Querkraft", [Hthm {guh = "thy_isac_B ...}],[]),

   346                          Ptyp ("Moment_Neigung", [Hthm {guh = "thy_isac_Biegeli...}],[]),

   347                    [])])])])]     : thehier ref *)

   348 the_hier (! thehier) (collect_thydata ());

   349 (*

   350 *** insert: preserved ["Isabelle"]

   351  *** insert: preserved ["Isabelle","HOL","Theorems","refl"]

   352  *** insert: preserved ["Isabelle","Fun","Theorems","o_apply"]

   353                 see WN120320.TODO check-improve rlsthmsNOTisac: ------\

   354  *** insert: preserved ["Isabelle","ListC","Theorems","del_base"]

   355  *** insert: preserved ["Isabelle","ListC","Theorems","del_rec"]

   356  *** insert: preserved ["Isabelle","ListC","Theorems","LENGTH_CONS"]

   357  *** insert: preserved ["Isabelle","ListC","Theorems","LENGTH_NIL"]

   358  *** insert: preserved ["Isabelle","ListC","Theorems","list_diff_def"]

   359                 see WN120320.TODO check-improve rlsthmsNOTisac: ------/

   360  *** insert: preserved ["Isabelle","List","Theorems","take_Nil"]

   361  *** insert: preserved ["Isabelle","List","Theorems","take_Cons"]

   362  *** insert: preserved ["Isabelle","List","Theorems","if_True"]

   363               Thm.get_name_hint @{t^^^^^^True} = "HOL.if_True";

   364  *** insert: preserved ["Isabelle","HOL","Theorems","if_False"]

   365  *** insert: preserved ["Isabelle","Rings","Theorems","distrib_right"]

   366  *** insert: preserved ["Isabelle","Rings","Theorems","distrib_left"]

   367  *** insert: preserved ["Isabelle","Groups","Theorems","mult_1_right"]

   368  *** insert: preserved ["Isabelle","Groups","Theorems","mult_1_left"]

   369  *** insert: preserved ["Isabelle","Rings","Theorems","mult_zero_left"]

   370  *** insert: preserved ["Isabelle","Rings","Theorems","mult_zero_right"]

   371  *** insert: preserved ["Isabelle","Groups","Theorems","add_0_left"]

   372  *** insert: preserved ["Isabelle","Groups","Theorems","add_0_right"]

   373  *** insert: preserved ["Isabelle","Rings","Theorems","divide_zero_left"]

   374  *** insert: preserved ["Isabelle","RealDef","Theorems","order_refl"]

   375  *** insert: preserved ["Isabelle","Groups","Theorems","minus_minus"]

   376  *** insert: preserved ["Isabelle","RealDef","Theorems","mult_commute"]

   377  *** insert: preserved ["Isabelle","RealDef","Theorems","mult_assoc"]

   378  *** insert: preserved ["Isabelle","Groups","Theorems","add_commute"]

   379  *** insert: preserved ["Isabelle","Groups","Theorems","add_left_commute"]

   380  *** insert: preserved ["Isabelle","Groups","Theorems","add_assoc"]

   381  *** insert: preserved ["Isabelle","Rings","Theorems","minus_mult_left"]

   382  *** insert: preserved ["Isabelle","Groups","Theorems","right_minus"]

   383  *** insert: preserved ["Isabelle","Rings","Theorems","left_diff_distrib"]

   384  *** insert: preserved ["Isabelle","Rings","Theorems","right_diff_distrib"]

   385  *** insert: preserved ["Isabelle","Rings","Theorems","minus_divide_left"]

   386  *** insert: preserved ["Isabelle","Rings","Theorems","times_divide_eq_right"]

   387  *** insert: preserved ["Isabelle","Fields","Theorems","times_divide_eq_left"]

   388  *** insert: preserved ["Isabelle","Fields","Theorems","divide_divide_eq_left"]

   389  *** insert: preserved ["Isabelle","Fields","Theorems","divide_divide_eq_right"]

   390  *** insert: preserved ["Isabelle","Rings","Theorems","divide_1"]

   391  *** insert: preserved ["Isabelle","Rings","Theorems","add_divide_distrib"]

   392  *** insert: preserved ["Isabelle","Int","Theorems","divide_minus1"]

   393  *** insert: preserved ["Isabelle","Groups","Theorems","neg_equal_iff_equal"]

   394                                                        ??? vvvvvvvvvvvvvv ------\

   395  *** insert: preserved ["IsacScripts","Script","Theorems","arity_type_ID"]

   396  *** insert: preserved ["IsacScripts","Script","Theorems","arity_type_arg"]

   397  *** insert: preserved ["IsacScripts","Tools","Theorems","arity_type_cpy"]

   398  *** insert: preserved ["IsacScripts","Tools","Theorems","arity_type_nam"]

   399  *** insert: preserved ["IsacScripts","Tools","Theorems","arity_type_str"]

   400  *** insert: preserved ["IsacScripts","Tools","Theorems","arity_type_una"]

   401  *** insert: preserved ["IsacScripts","Tools","Theorems","arity_type_unl"]

   402  *** insert: preserved ["IsacScripts","Tools","Theorems","arity_type_toreal"]

   403  *** insert: preserved ["IsacScripts","Tools","Theorems","arity_type_unknow"]

   404  *** insert: preserved ["IsacScripts","Tools","Theorems","arity_type_tobooll"]

   405  *** insert: preserved ["IsacScripts","Tools","Theorems","arity_type_toreall"]

   406                                                        ??? vvvvvvvvvvvvvv ------/

   407  *** insert: preserved ["IsacScripts","Tools","Rulesets","e_rls"]

   408  *** insert: preserved ["IsacScripts","Tools","Rulesets","e_rrls"]

   409                  see WN120320.TODO check-improve rlsthmsNOTisac: ------\

   410  *** insert: preserved ["IsacScripts","ListC","Theorems","LAST"]  = ["IsacKnowledge","ListC"---\

   411  *** insert: preserved ["IsacScripts","ListC","Theorems","hd_thm"]

   412  *** insert: preserved ["IsacScripts","ListC","Theorems","tl_Nil"]

   413  *** insert: preserved ["IsacScripts","ListC","Theorems","NTH_NIL"]

   414  *** insert: preserved ["IsacScripts","ListC","Theorems","del_def"]

   415  *** insert: preserved ["IsacScripts","ListC","Theorems","map_Nil"]

   416  *** insert: preserved ["IsacScripts","ListC","Theorems","mem_Nil"]

   417  *** insert: preserved ["IsacScripts","ListC","Theorems","rev_Nil"]

   418  *** insert: preserved ["IsacScripts","ListC","Theorems","tl_Cons"]

   419  *** insert: preserved ["IsacScripts","ListC","Theorems","zip_Nil"]

   420  *** insert: preserved ["IsacScripts","ListC","Theorems","NTH_CONS"]

   421  *** insert: preserved ["IsacScripts","ListC","Theorems","map_Cons"]

   422  *** insert: preserved ["IsacScripts","ListC","Theorems","mem_Cons"]

   423  *** insert: preserved ["IsacScripts","ListC","Theorems","null_Nil"]

   424  *** insert: preserved ["IsacScripts","ListC","Theorems","rev_Cons"]

   425  *** insert: preserved ["IsacScripts","ListC","Theorems","zip_Cons"]

   426  *** insert: preserved ["IsacScripts","ListC","Theorems","foldr_Nil"]

   427  *** insert: preserved ["IsacScripts","ListC","Theorems","null_Cons"]

   428  *** insert: preserved ["IsacScripts","ListC","Theorems","LENGTH_def"]

   429  *** insert: preserved ["IsacScripts","ListC","Theorems","append_Nil"]

   430  *** insert: preserved ["IsacScripts","ListC","Theorems","concat_Nil"]

   431  *** insert: preserved ["IsacScripts","ListC","Theorems","filter_Nil"]

   432  *** insert: preserved ["IsacScripts","ListC","Theorems","foldr_Cons"]

   433  *** insert: preserved ["IsacScripts","ListC","Theorems","append_Cons"]

   434  *** insert: preserved ["IsacScripts","ListC","Theorems","butlast_Nil"]

   435  *** insert: preserved ["IsacScripts","ListC","Theorems","concat_Cons"]

   436  *** insert: preserved ["IsacScripts","ListC","Theorems","filter_Cons"]

   437  *** insert: preserved ["IsacScripts","ListC","Theorems","remdups_Nil"]

   438  *** insert: preserved ["IsacScripts","ListC","Theorems","butlast_Cons"]

   439  *** insert: preserved ["IsacScripts","ListC","Theorems","distinct_Nil"]

   440  *** insert: preserved ["IsacScripts","ListC","Theorems","remdups_Cons"]

   441  *** insert: preserved ["IsacScripts","ListC","Theorems","distinct_Cons"]

   442  *** insert: preserved ["IsacScripts","ListC","Theorems","dropWhile_Nil"]

   443  *** insert: preserved ["IsacScripts","ListC","Theorems","takeWhile_Nil"]

   444  *** insert: preserved ["IsacScripts","ListC","Theorems","dropWhile_Cons"]

   445  *** insert: preserved ["IsacScripts","ListC","Theorems","takeWhile_Cons"]

   446  *** insert: preserved ["IsacScripts","ListC","Theorems","list_diff_def_raw"] =["IsacKnowledge"---/

   447  *** insert: preserved ["IsacKnowledge","Inverse_Z_Transform","Theorems","rule1"]

   448  *** insert: preserved ["IsacKnowledge","Inverse_Z_Transform","Theorems","rule2"]

   449  *** insert: preserved ["IsacKnowledge","Inverse_Z_Transform","Theorems","rule3"]

   450  *** insert: preserved ["IsacKnowledge","Inverse_Z_Transform","Theorems","rule4"]

   451  *** insert: preserved ["IsacKnowledge","Inverse_Z_Transform","Theorems","rule5"]

   452  *** insert: preserved ["IsacKnowledge","Inverse_Z_Transform","Theorems","rule6"]

   453  *** insert: preserved ["IsacKnowledge","Inverse_Z_Transform","Theorems","ruleYZ"]

   454  *** insert: preserved ["IsacKnowledge","Inverse_Z_Transform","Theorems","ruleZY"]

   455  *** insert: preserved ["IsacKnowledge","Inverse_Z_Transform","Rulesets","inverse_z"]

   456  *** insert: preserved ["IsacKnowledge","DiophantEq","Theorems","int_isolate_add"]

   457  *** insert: preserved ["IsacKnowledge","Biegelinie","Theorems","Moment_Neigung"]

   458  *** insert: preserved ["IsacKnowledge","Biegelinie","Theorems","Neigung_Moment"]

   459  *** insert: preserved ["IsacKnowledge","Biegelinie","Theorems","Moment_Querkraft"]

   460  *** insert: preserved ["IsacKnowledge","Biegelinie","Theorems","Querkraft_Moment"]

   461  *** insert: preserved ["IsacKnowledge","Biegelinie","Theorems","make_fun_explicit"]

   462  *** insert: preserved ["IsacKnowledge","Biegelinie","Theorems","Belastung_Querkraft"]

   463  *** insert: preserved ["IsacKnowledge","Biegelinie","Theorems","Querkraft_Belastung"]

   464  *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","x_quadrat"]

   465  *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","null_minus"]

   466  *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","subtrahiere"]

   467  *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","tausche_mal"]

   468  *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","tausche_plus"]

   469  *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","subtrahiere_1"]

   470  *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","tausche_minus"]

   471  *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","vor_minus_mal"]

   472  *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","tausche_mal_mal"]

   473  *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","tausche_vor_mal"]

   474  *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","tausche_vor_plus"]

   475  *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","addiere_vor_minus"]

   476  *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","subtrahiere_von_1"]

   477  *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","tausche_plus_plus"]

   478  *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","tausche_vor_minus"]

   479  *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","klammer_minus_mult"]

   480  *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","klammer_minus_plus"]

   481  *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","klammer_mult_minus"]

   482  *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","klammer_plus_minus"]

   483  *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","tausche_minus_plus"]

   484  *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","tausche_plus_minus"]

   485  *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","klammer_minus_minus"]

   486  *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","tausche_minus_minus"]

   487  *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","subtrahiere_vor_minus"]

   488  *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","vorzeichen_minus_weg1"]

   489  *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","vorzeichen_minus_weg2"]

   490  *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","vorzeichen_minus_weg3"]

   491  *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","vorzeichen_minus_weg4"]

   492  *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","addiere_eins_vor_minus"]

   493  *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","subtrahiere_x_minus_plus"]

   494  *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","subtrahiere_x_plus_minus"]

   495  *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","subtrahiere_x_minus1_plus"]

   496  *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","subtrahiere_x_minus_minus"]

   497  *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","subtrahiere_x_minus_plus1"]

   498  *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","subtrahiere_x_plus1_minus"]

   499  *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","subtrahiere_x_plus_minus1"]

   500  *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","subtrahiere_eins_vor_minus"]

   501  *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","subtrahiere_x_minus1_minus"]

   502  *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","subtrahiere_x_minus_minus1"]

   503  *** insert: preserved ["IsacKnowledge","PolyMinus","Rulesets","ordne_alphabetisch"]

   504  *** insert: preserved ["IsacKnowledge","PolyMinus","Rulesets","fasse_zusammen"]

   505  *** insert: preserved ["IsacKnowledge","PolyMinus","Rulesets","verschoenere"]

   506  *** insert: preserved ["IsacKnowledge","PolyMinus","Rulesets","ordne_monome"]

   507  *** insert: preserved ["IsacKnowledge","PolyMinus","Rulesets","klammern_aufloesen"]

   508  *** insert: preserved ["IsacKnowledge","PolyMinus","Rulesets","klammern_ausmultiplizieren"]

   509  *** insert: preserved ["IsacKnowledge","Partial_Fractions","Theorems","ansatz_2nd_order"]

   510  *** insert: preserved ["IsacKnowledge","Partial_Fractions","Theorems","ansatz_3rd_order"]

   511  *** insert: preserved ["IsacKnowledge","Partial_Fractions","Theorems","ansatz_4th_order"]

   512  *** insert: preserved ["IsacKnowledge","Partial_Fractions","Theorems","multiply_2nd_order"]

   513  *** insert: preserved ["IsacKnowledge","Partial_Fractions","Theorems","multiply_3rd_order"]

   514  *** insert: preserved ["IsacKnowledge","Partial_Fractions","Theorems","multiply_4th_order"]

   515  *** insert: preserved ["IsacKnowledge","Partial_Fractions","Theorems","equival_trans_2nd_order"]

   516  *** insert: preserved ["IsacKnowledge","Partial_Fractions","Theorems","equival_trans_3rd_order"]

   517  *** insert: preserved ["IsacKnowledge","Partial_Fractions","Theorems","equival_trans_4th_order"]

   518  *** insert: preserved ["IsacKnowledge","Partial_Fractions","Rulesets","ansatz_rls"]

   519  *** insert: preserved ["IsacKnowledge","Partial_Fractions","Rulesets","multiply_ansatz"]

   520  *** insert: preserved ["IsacKnowledge","Partial_Fractions","Rulesets","equival_trans"]

   521  *** insert: preserved ["IsacKnowledge","DiffApp","Theorems","filterVar_Nil"]

   522  *** insert: preserved ["IsacKnowledge","DiffApp","Theorems","filterVar_Const"]

   523  *** insert: preserved ["IsacKnowledge","DiffApp","Rulesets","list_rls"]

   524  *** insert: preserved ["IsacKnowledge","DiffApp","Rulesets","eval_rls"]

   525  *** insert: preserved ["IsacKnowledge","Test","Theorems","radd_0"]

   526  *** insert: preserved ["IsacKnowledge","Test","Theorems","rsqare"]

   527  *** insert: preserved ["IsacKnowledge","Test","Theorems","exp_pow"]

   528  *** insert: preserved ["IsacKnowledge","Test","Theorems","power_1"]

   529  *** insert: preserved ["IsacKnowledge","Test","Theorems","rmult_0"]

   530  *** insert: preserved ["IsacKnowledge","Test","Theorems","rmult_1"]

   531  *** insert: preserved ["IsacKnowledge","Test","Theorems","root_ge0"]

   532  *** insert: preserved ["IsacKnowledge","Test","Theorems","radd_assoc"]

   533  *** insert: preserved ["IsacKnowledge","Test","Theorems","root_ge0_1"]

   534  *** insert: preserved ["IsacKnowledge","Test","Theorems","root_ge0_2"]

   535  *** insert: preserved ["IsacKnowledge","Test","Theorems","mult_square"]

   536  *** insert: preserved ["IsacKnowledge","Test","Theorems","rcancel_den"]

   537  *** insert: preserved ["IsacKnowledge","Test","Theorems","rmult_assoc"]

   538  *** insert: preserved ["IsacKnowledge","Test","Theorems","radd_0_right"]

   539  *** insert: preserved ["IsacKnowledge","Test","Theorems","radd_commute"]

   540  *** insert: preserved ["IsacKnowledge","Test","Theorems","root_add_ge0"]

   541  *** insert: preserved ["IsacKnowledge","Test","Theorems","rroot_to_lhs"]

   542  *** insert: preserved ["IsacKnowledge","Test","Theorems","rcancel_const"]

   543  *** insert: preserved ["IsacKnowledge","Test","Theorems","rmult_0_right"]

   544  *** insert: preserved ["IsacKnowledge","Test","Theorems","rmult_1_right"]

   545  *** insert: preserved ["IsacKnowledge","Test","Theorems","rmult_commute"]

   546  *** insert: preserved ["IsacKnowledge","Test","Theorems","rbinom_power_2"]

   547  *** insert: preserved ["IsacKnowledge","Test","Theorems","rcollect_right"]

   548  *** insert: preserved ["IsacKnowledge","Test","Theorems","constant_square"]

   549  *** insert: preserved ["IsacKnowledge","Test","Theorems","radd_real_const"]

   550  *** insert: preserved ["IsacKnowledge","Test","Theorems","square_equality"]

   551  *** insert: preserved ["IsacKnowledge","Test","Theorems","square_equation"]

   552  *** insert: preserved ["IsacKnowledge","Test","Theorems","rdistr_div_right"]

   553  *** insert: preserved ["IsacKnowledge","Test","Theorems","risolate_bdv_add"]

   554  *** insert: preserved ["IsacKnowledge","Test","Theorems","rroot_square_inv"]

   555  *** insert: preserved ["IsacKnowledge","Test","Theorems","rroot_times_root"]

   556  *** insert: preserved ["IsacKnowledge","Test","Theorems","rshift_nominator"]

   557  *** insert: preserved ["IsacKnowledge","Test","Theorems","rtwo_of_the_same"]

   558  *** insert: preserved ["IsacKnowledge","Test","Theorems","radd_left_commute"]

   559  *** insert: preserved ["IsacKnowledge","Test","Theorems","rcollect_one_left"]

   560  *** insert: preserved ["IsacKnowledge","Test","Theorems","risolate_bdv_mult"]

   561  *** insert: preserved ["IsacKnowledge","Test","Theorems","risolate_root_add"]

   562  *** insert: preserved ["IsacKnowledge","Test","Theorems","risolate_root_div"]

   563  *** insert: preserved ["IsacKnowledge","Test","Theorems","rroot_to_lhs_mult"]

   564  *** insert: preserved ["IsacKnowledge","Test","Theorems","square_equality_0"]

   565  *** insert: preserved ["IsacKnowledge","Test","Theorems","radd_mult_distrib2"]

   566  *** insert: preserved ["IsacKnowledge","Test","Theorems","radd_real_const_eq"]

   567  *** insert: preserved ["IsacKnowledge","Test","Theorems","rdistr_right_assoc"]

   568  *** insert: preserved ["IsacKnowledge","Test","Theorems","risolate_root_mult"]

   569  *** insert: preserved ["IsacKnowledge","Test","Theorems","rmult_left_commute"]

   570  *** insert: preserved ["IsacKnowledge","Test","Theorems","rnorm_equation_add"]

   571  *** insert: preserved ["IsacKnowledge","Test","Theorems","constant_mult_square"]

   572  *** insert: preserved ["IsacKnowledge","Test","Theorems","rdistr_right_assoc_p"]

   573  *** insert: preserved ["IsacKnowledge","Test","Theorems","square_equation_left"]

   574  *** insert: preserved ["IsacKnowledge","Test","Theorems","risolate_bdv_mult_add"]

   575  *** insert: preserved ["IsacKnowledge","Test","Theorems","rroot_to_lhs_add_mult"]

   576  *** insert: preserved ["IsacKnowledge","Test","Theorems","square_equation_right"]

   577  *** insert: preserved ["IsacKnowledge","Test","Theorems","rroot_times_root_assoc"]

   578  *** insert: preserved ["IsacKnowledge","Test","Theorems","rtwo_of_the_same_assoc"]

   579  *** insert: preserved ["IsacKnowledge","Test","Theorems","rcollect_one_left_assoc"]

   580  *** insert: preserved ["IsacKnowledge","Test","Theorems","rroot_times_root_assoc_p"]

   581  *** insert: preserved ["IsacKnowledge","Test","Theorems","rtwo_of_the_same_assoc_p"]

   582  *** insert: preserved ["IsacKnowledge","Test","Theorems","rcollect_one_left_assoc_p"]

   583  *** insert: preserved ["IsacKnowledge","Test","Rulesets","testerls"]

   584  *** insert: preserved ["IsacKnowledge","Test","Rulesets","Test_simplify"]

   585  *** insert: preserved ["IsacKnowledge","Test","Rulesets","tval_rls"]

   586  *** insert: preserved ["IsacKnowledge","Test","Rulesets","isolate_root"]

   587  *** insert: preserved ["IsacKnowledge","Test","Rulesets","isolate_bdv"]

   588  *** insert: preserved ["IsacKnowledge","Test","Rulesets","matches"]

   589  *** insert: preserved ["IsacKnowledge","Test","Rulesets","norm_equation"]

   590  *** insert: preserved ["IsacKnowledge","Test","Rulesets","ac_plus_times"]

   591  *** insert: preserved ["IsacKnowledge","Test","Rulesets","rearrange_assoc"]

   592  *** insert: preserved ["IsacKnowledge","Test","Rulesets","make_polytest"]

   593  *** insert: preserved ["IsacKnowledge","Test","Rulesets","expand_binomtest"]

   594  *** insert: preserved ["IsacKnowledge","EqSystem","Theorems","separate_bdvs0"]

   595  *** insert: preserved ["IsacKnowledge","EqSystem","Theorems","order_system_NxN"]

   596  *** insert: preserved ["IsacKnowledge","EqSystem","Theorems","separate_bdvs_add"]

   597  *** insert: preserved ["IsacKnowledge","EqSystem","Theorems","commute_0_equality"]

   598  *** insert: preserved ["IsacKnowledge","EqSystem","Theorems","separate_bdvs_add1"]

   599  *** insert: preserved ["IsacKnowledge","EqSystem","Theorems","separate_bdvs_add2"]

   600  *** insert: preserved ["IsacKnowledge","EqSystem","Theorems","separate_bdvs_mult"]

   601  *** insert: preserved ["IsacKnowledge","EqSystem","Rulesets","simplify_System_parenthesized"]

   602  *** insert: preserved ["IsacKnowledge","EqSystem","Rulesets","simplify_System"]

   603  *** insert: preserved ["IsacKnowledge","EqSystem","Rulesets","isolate_bdvs"]

   604  *** insert: preserved ["IsacKnowledge","EqSystem","Rulesets","isolate_bdvs_4x4"]

   605  *** insert: preserved ["IsacKnowledge","EqSystem","Rulesets","order_system"]

   606  *** insert: preserved ["IsacKnowledge","EqSystem","Rulesets","order_add_mult_System"]

   607  *** insert: preserved ["IsacKnowledge","EqSystem","Rulesets","norm_System_noadd_fractions"]

   608  *** insert: preserved ["IsacKnowledge","EqSystem","Rulesets","norm_System"]

   609  *** insert: preserved ["IsacKnowledge","Integrate","Theorems","integral_add"]

   610  *** insert: preserved ["IsacKnowledge","Integrate","Theorems","integral_pow"]

   611  *** insert: preserved ["IsacKnowledge","Integrate","Theorems","integral_var"]

   612  *** insert: preserved ["IsacKnowledge","Integrate","Theorems","integral_mult"]

   613  *** insert: preserved ["IsacKnowledge","Integrate","Theorems","integral_const"]

   614  *** insert: preserved ["IsacKnowledge","Integrate","Rulesets","integration_rules"]

   615  *** insert: preserved ["IsacKnowledge","Integrate","Rulesets","add_new_c"]

   616  *** insert: preserved ["IsacKnowledge","Integrate","Rulesets","simplify_Integral"]

   617  *** insert: preserved ["IsacKnowledge","Integrate","Rulesets","integration"]

   618  *** insert: preserved ["IsacKnowledge","Integrate","Rulesets","separate_bdv2"]

   619  *** insert: preserved ["IsacKnowledge","Integrate","Rulesets","norm_Rational_noadd_fractions"]

   620  *** insert: preserved ["IsacKnowledge","Integrate","Rulesets","norm_Rational_rls_noadd_fractions"]

   621  *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_ln"]

   622  *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_cos"]

   623  *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_dif"]

   624  *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_exp"]

   625  *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_pow"]

   626  *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_sin"]

   627  *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_sum"]

   628  *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_var"]

   629  *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_prod"]

   630  *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_quot"]

   631  *** insert: preserved ["IsacKnowledge","Diff","Theorems","frac_conv"]

   632  *** insert: preserved ["IsacKnowledge","Diff","Theorems","root_conv"]

   633  *** insert: preserved ["IsacKnowledge","Diff","Theorems","sqrt_conv"]

   634  *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_const"]

   635  *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_ln_chain"]

   636  *** insert: preserved ["IsacKnowledge","Diff","Theorems","frac_sym_conv"]

   637  *** insert: preserved ["IsacKnowledge","Diff","Theorems","root_sym_conv"]

   638  *** insert: preserved ["IsacKnowledge","Diff","Theorems","sqrt_conv_bdv"]

   639  *** insert: preserved ["IsacKnowledge","Diff","Theorems","sqrt_sym_conv"]

   640  *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_cos_chain"]

   641  *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_exp_chain"]

   642  *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_pow_chain"]

   643  *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_sin_chain"]

   644  *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_prod_const"]

   645  *** insert: preserved ["IsacKnowledge","Diff","Theorems","realpow_pow_bdv"]

   646  *** insert: preserved ["IsacKnowledge","Diff","Theorems","sqrt_conv_bdv_n"]

   647  *** insert: preserved ["IsacKnowledge","Diff","Rulesets","diff_rules"]

   648  *** insert: preserved ["IsacKnowledge","Diff","Rulesets","norm_diff"]

   649  *** insert: preserved ["IsacKnowledge","Diff","Rulesets","diff_conv"]

   650  *** insert: preserved ["IsacKnowledge","Diff","Rulesets","diff_sym_conv"]

   651  *** insert: preserved ["IsacKnowledge","Diff","Rulesets","erls"]

   652  *** insert: preserved ["IsacKnowledge","LogExp","Theorems","equality_pow"]

   653  *** insert: preserved ["IsacKnowledge","LogExp","Theorems","equality_power"]

   654  *** insert: preserved ["IsacKnowledge","LogExp","Theorems","exp_invers_log"]

   655  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d0_true"]

   656  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","all_left"]

   657  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d0_false"]

   658  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","makex1_x"]

   659  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","plus_leq"]

   660  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d4_sub_u1"]

   661  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","minus_leq"]

   662  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_prescind1"]

   663  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_prescind2"]

   664  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_prescind3"]

   665  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_prescind4"]

   666  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","real_assoc_1"]

   667  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","real_assoc_2"]

   668  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","separate_bdv"]

   669  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_collect_1"]

   670  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_collect_2"]

   671  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_collect_3"]

   672  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_explicit1"]

   673  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_explicit2"]

   674  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_explicit3"]

   675  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula1"]

   676  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula2"]

   677  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula3"]

   678  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula4"]

   679  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula5"]

   680  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula6"]

   681  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula7"]

   682  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula8"]

   683  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula9"]

   684  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d1_isolate_div"]

   685  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula1"]

   686  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula2"]

   687  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula3"]

   688  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula4"]

   689  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula5"]

   690  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula6"]

   691  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula7"]

   692  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula8"]

   693  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula9"]

   694  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_isolate_div"]

   695  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula10"]

   696  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_isolate_div"]

   697  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","real_minus_div"]

   698  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","separate_1_bdv"]

   699  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","separate_bdv_n"]

   700  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_n_collect_1"]

   701  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_n_collect_2"]

   702  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_n_collect_3"]

   703  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d1_isolate_add1"]

   704  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d1_isolate_add2"]

   705  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula10"]

   706  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_isolate_add1"]

   707  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_isolate_add2"]

   708  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_isolate_add1"]

   709  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_isolate_add2"]

   710  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","complete_square1"]

   711  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","complete_square2"]

   712  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","complete_square3"]

   713  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","complete_square4"]

   714  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","complete_square5"]

   715  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","separate_1_bdv_n"]

   716  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","square_explicit1"]

   717  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","square_explicit2"]

   718  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula1_neg"]

   719  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula2_neg"]

   720  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula3_neg"]

   721  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula4_neg"]

   722  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula9_neg"]

   723  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_sqrt_equation1"]

   724  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_sqrt_equation2"]

   725  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_sqrt_equation3"]

   726  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_root_equation1"]

   727  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_root_equation2"]

   728  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula1_neg"]

   729  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula2_neg"]

   730  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula3_neg"]

   731  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula4_neg"]

   732  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula5_neg"]

   733  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula6_neg"]

   734  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula10_neg"]

   735  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_reduce_equation1"]

   736  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_reduce_equation2"]

   737  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation1"]

   738  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation2"]

   739  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation3"]

   740  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation4"]

   741  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation5"]

   742  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation6"]

   743  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation7"]

   744  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation8"]

   745  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation9"]

   746  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_collect_assoc1_1"]

   747  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_collect_assoc1_2"]

   748  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_collect_assoc1_3"]

   749  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_collect_assoc2_1"]

   750  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_collect_assoc2_2"]

   751  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_collect_assoc2_3"]

   752  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation10"]

   753  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation11"]

   754  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation12"]

   755  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation13"]

   756  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation14"]

   757  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation15"]

   758  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation16"]

   759  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","cancel_leading_coeff1"]

   760  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","cancel_leading_coeff2"]

   761  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","cancel_leading_coeff3"]

   762  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","cancel_leading_coeff4"]

   763  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","cancel_leading_coeff5"]

   764  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","cancel_leading_coeff6"]

   765  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","cancel_leading_coeff7"]

   766  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","cancel_leading_coeff8"]

   767  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","cancel_leading_coeff9"]

   768  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_sqrt_equation1_neg"]

   769  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_n_collect_assoc1_1"]

   770  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_n_collect_assoc1_2"]

   771  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_n_collect_assoc1_3"]

   772  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_n_collect_assoc2_1"]

   773  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_n_collect_assoc2_2"]

   774  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_n_collect_assoc2_3"]

   775  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","cancel_leading_coeff10"]

   776  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","cancel_leading_coeff11"]

   777  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","cancel_leading_coeff12"]

   778  *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","cancel_leading_coeff13"]

   779  *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","cancel_leading_coeff"]

   780  *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","complete_square"]

   781  *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","PolyEq_erls"]

   782  *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","polyeq_simplify"]

   783  *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","d0_polyeq_simplify"]

   784  *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","d1_polyeq_simplify"]

   785  *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","d2_polyeq_simplify"]

   786  *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","d2_polyeq_bdv_only_simplify"]

   787  *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","d2_polyeq_sq_only_simplify"]

   788  *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","d2_polyeq_pqFormula_simplify"]

   789  *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","d2_polyeq_abcFormula_simplify"]

   790  *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","d3_polyeq_simplify"]

   791  *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","d4_polyeq_simplify"]

   792  *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","order_add_mult_in"]

   793  *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","collect_bdv"]

   794  *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","make_polynomial_in"]

   795  *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","make_ratpoly_in"]

   796  *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","separate_bdvs"]

   797  *** insert: preserved ["IsacKnowledge","RootRatEq","Theorems","rootrat_equation_left_1"]

   798  *** insert: preserved ["IsacKnowledge","RootRatEq","Theorems","rootrat_equation_left_2"]

   799  *** insert: preserved ["IsacKnowledge","RootRatEq","Theorems","rootrat_equation_right_1"]

   800  *** insert: preserved ["IsacKnowledge","RootRatEq","Theorems","rootrat_equation_right_2"]

   801  *** insert: preserved ["IsacKnowledge","RootRatEq","Rulesets","RooRatEq_erls"]

   802  *** insert: preserved ["IsacKnowledge","RootRatEq","Rulesets","rootrat_solve"]

   803  *** insert: preserved ["IsacKnowledge","RootRat","Rulesets","rootrat_erls"]

   804  *** insert: preserved ["IsacKnowledge","RootRat","Rulesets","calculate_RootRat"]

   805  *** insert: preserved ["IsacKnowledge","RatEq","Theorems","real_rat_pow"]

   806  *** insert: preserved ["IsacKnowledge","RatEq","Theorems","real_rat_mult_1"]

   807  *** insert: preserved ["IsacKnowledge","RatEq","Theorems","real_rat_mult_2"]

   808  *** insert: preserved ["IsacKnowledge","RatEq","Theorems","real_rat_mult_3"]

   809  *** insert: preserved ["IsacKnowledge","RatEq","Theorems","rat_double_rat_1"]

   810  *** insert: preserved ["IsacKnowledge","RatEq","Theorems","rat_double_rat_2"]

   811  *** insert: preserved ["IsacKnowledge","RatEq","Theorems","rat_double_rat_3"]

   812  *** insert: preserved ["IsacKnowledge","RatEq","Theorems","rat_mult_denominator_both"]

   813  *** insert: preserved ["IsacKnowledge","RatEq","Theorems","rat_mult_denominator_left"]

   814  *** insert: preserved ["IsacKnowledge","RatEq","Theorems","rat_mult_denominator_right"]

   815  *** insert: preserved ["IsacKnowledge","RatEq","Rulesets","rateq_erls"]

   816  *** insert: preserved ["IsacKnowledge","RatEq","Rulesets","RatEq_eliminate"]

   817  *** insert: preserved ["IsacKnowledge","RatEq","Rulesets","RatEq_simplify"]

   818  *** insert: preserved ["IsacKnowledge","RootEq","Theorems","makex1_x"]

   819  *** insert: preserved ["IsacKnowledge","RootEq","Theorems","real_assoc_1"]

   820  *** insert: preserved ["IsacKnowledge","RootEq","Theorems","real_assoc_2"]

   821  *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_1"]

   822  *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_2"]

   823  *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_times_root_1"]

   824  *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_times_root_2"]

   825  *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_isolate_l_add1"]

   826  *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_isolate_l_add2"]

   827  *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_isolate_l_add3"]

   828  *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_isolate_l_add4"]

   829  *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_isolate_l_add5"]

   830  *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_isolate_l_add6"]

   831  *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_isolate_r_add1"]

   832  *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_isolate_r_add2"]

   833  *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_isolate_r_add3"]

   834  *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_isolate_r_add4"]

   835  *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_isolate_r_add5"]

   836  *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_isolate_r_add6"]

   837  *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_both_1"]

   838  *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_both_2"]

   839  *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_both_3"]

   840  *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_both_4"]

   841  *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_left_1"]

   842  *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_left_2"]

   843  *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_left_3"]

   844  *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_left_4"]

   845  *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_left_5"]

   846  *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_left_6"]

   847  *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_right_1"]

   848  *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_right_2"]

   849  *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_right_3"]

   850  *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_right_4"]

   851  *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_right_5"]

   852  *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_right_6"]

   853  *** insert: preserved ["IsacKnowledge","RootEq","Rulesets","RootEq_erls"]

   854  *** insert: preserved ["IsacKnowledge","RootEq","Rulesets","rooteq_srls"]

   855  *** insert: preserved ["IsacKnowledge","RootEq","Rulesets","sqrt_isolate"]

   856  *** insert: preserved ["IsacKnowledge","RootEq","Rulesets","l_sqrt_isolate"]

   857  *** insert: preserved ["IsacKnowledge","RootEq","Rulesets","r_sqrt_isolate"]

   858  *** insert: preserved ["IsacKnowledge","RootEq","Rulesets","rooteq_simplify"]

   859  *** insert: preserved ["IsacKnowledge","LinEq","Theorems","all_left"]

   860  *** insert: preserved ["IsacKnowledge","LinEq","Theorems","makex1_x"]

   861  *** insert: preserved ["IsacKnowledge","LinEq","Theorems","real_assoc_1"]

   862  *** insert: preserved ["IsacKnowledge","LinEq","Theorems","real_assoc_2"]

   863  *** insert: preserved ["IsacKnowledge","LinEq","Theorems","lin_isolate_div"]

   864  *** insert: preserved ["IsacKnowledge","LinEq","Theorems","lin_isolate_add1"]

   865  *** insert: preserved ["IsacKnowledge","LinEq","Theorems","lin_isolate_add2"]

   866  *** insert: preserved ["IsacKnowledge","LinEq","Rulesets","LinEq_erls"]

   867  *** insert: preserved ["IsacKnowledge","LinEq","Rulesets","LinPoly_simplify"]

   868  *** insert: preserved ["IsacKnowledge","LinEq","Rulesets","LinEq_simplify"]

   869  *** insert: preserved ["IsacKnowledge","Root","Theorems","root_false"]

   870  *** insert: preserved ["IsacKnowledge","Root","Theorems","realpow_mul"]

   871  *** insert: preserved ["IsacKnowledge","Root","Theorems","real_diff_minus"]

   872  *** insert: preserved ["IsacKnowledge","Root","Theorems","root_plus_minus"]

   873  *** insert: preserved ["IsacKnowledge","Root","Theorems","real_root_negative"]

   874  *** insert: preserved ["IsacKnowledge","Root","Theorems","real_root_positive"]

   875  *** insert: preserved ["IsacKnowledge","Root","Theorems","real_mm_binom_times"]

   876  *** insert: preserved ["IsacKnowledge","Root","Theorems","real_mp_binom_times"]

   877  *** insert: preserved ["IsacKnowledge","Root","Theorems","real_pm_binom_times"]

   878  *** insert: preserved ["IsacKnowledge","Root","Theorems","real_pp_binom_times"]

   879  *** insert: preserved ["IsacKnowledge","Root","Theorems","real_plus_binom_pow2"]

   880  *** insert: preserved ["IsacKnowledge","Root","Theorems","real_plus_binom_pow3"]

   881  *** insert: preserved ["IsacKnowledge","Root","Theorems","real_minus_binom_pow2"]

   882  *** insert: preserved ["IsacKnowledge","Root","Theorems","real_minus_binom_pow3"]

   883  *** insert: preserved ["IsacKnowledge","Root","Theorems","real_plus_binom_times"]

   884  *** insert: preserved ["IsacKnowledge","Root","Theorems","real_minus_binom_times"]

   885  *** insert: preserved ["IsacKnowledge","Root","Theorems","real_plus_minus_binom1"]

   886  *** insert: preserved ["IsacKnowledge","Root","Theorems","real_plus_minus_binom2"]

   887  *** insert: preserved ["IsacKnowledge","Root","Rulesets","Root_erls"]

   888  *** insert: preserved ["IsacKnowledge","Root","Rulesets","make_rooteq"]

   889  *** insert: preserved ["IsacKnowledge","Root","Rulesets","expand_rootbinoms"]

   890  *** insert: preserved ["IsacKnowledge","Equation","Rulesets","univariate_equation_prls"]

   891  *** insert: preserved ["IsacKnowledge","Rational","Theorems","rat_add"]

   892  *** insert: preserved ["IsacKnowledge","Rational","Theorems","rat_add1"]

   893  *** insert: preserved ["IsacKnowledge","Rational","Theorems","rat_add2"]

   894  *** insert: preserved ["IsacKnowledge","Rational","Theorems","rat_add3"]

   895  *** insert: preserved ["IsacKnowledge","Rational","Theorems","rat_mult"]

   896  *** insert: preserved ["IsacKnowledge","Rational","Theorems","add_minus"]

   897  *** insert: preserved ["IsacKnowledge","Rational","Theorems","rat_mult2"]

   898  *** insert: preserved ["IsacKnowledge","Rational","Theorems","rat_power"]

   899  *** insert: preserved ["IsacKnowledge","Rational","Theorems","add_minus1"]

   900  *** insert: preserved ["IsacKnowledge","Rational","Theorems","mult_cross"]

   901  *** insert: preserved ["IsacKnowledge","Rational","Theorems","mult_cross1"]

   902  *** insert: preserved ["IsacKnowledge","Rational","Theorems","mult_cross2"]

   903  *** insert: preserved ["IsacKnowledge","Rational","Theorems","rat_add_assoc"]

   904  *** insert: preserved ["IsacKnowledge","Rational","Theorems","rat_add1_assoc"]

   905  *** insert: preserved ["IsacKnowledge","Rational","Theorems","rat_add2_assoc"]

   906  *** insert: preserved ["IsacKnowledge","Rational","Theorems","rat_add3_assoc"]

   907  *** insert: preserved ["IsacKnowledge","Rational","Theorems","rat_mult_poly_l"]

   908  *** insert: preserved ["IsacKnowledge","Rational","Theorems","rat_mult_poly_r"]

   909  *** insert: preserved ["IsacKnowledge","Rational","Theorems","real_divide_divide1"]

   910  *** insert: preserved ["IsacKnowledge","Rational","Theorems","real_mult_div_cancel2"]

   911  *** insert: preserved ["IsacKnowledge","Rational","Theorems","real_times_divide_num"]

   912  *** insert: preserved ["IsacKnowledge","Rational","Theorems","real_divide_divide1_mg"]

   913  *** insert: preserved ["IsacKnowledge","Rational","Theorems","real_times_divide_1_eq"]

   914  *** insert: preserved ["IsacKnowledge","Rational","Rulesets","discard_minus"]

   915  *** insert: preserved ["IsacKnowledge","Rational","Rulesets","calculate_Rational"]

   916  *** insert: preserved ["IsacKnowledge","Rational","Rulesets","calc_rat_erls"]

   917  *** insert: preserved ["IsacKnowledge","Rational","Rulesets","rational_erls"]

   918  *** insert: preserved ["IsacKnowledge","Rational","Rulesets","cancel_p"]

   919  *** insert: preserved ["IsacKnowledge","Rational","Rulesets","cancel"]

   920  *** insert: preserved ["IsacKnowledge","Rational","Rulesets","add_fractions_p"]

   921  *** insert: preserved ["IsacKnowledge","Rational","Rulesets","add_fractions_p_rls"]

   922  *** insert: preserved ["IsacKnowledge","Rational","Rulesets","common_nominator"]

   923  *** insert: preserved ["IsacKnowledge","Rational","Rulesets","powers_erls"]

   924  *** insert: preserved ["IsacKnowledge","Rational","Rulesets","powers"]

   925  *** insert: preserved ["IsacKnowledge","Rational","Rulesets","rat_mult_divide"]

   926  *** insert: preserved ["IsacKnowledge","Rational","Rulesets","reduce_0_1_2"]

   927  *** insert: preserved ["IsacKnowledge","Rational","Rulesets","rat_reduce_1"]

   928  *** insert: preserved ["IsacKnowledge","Rational","Rulesets","norm_rat_erls"]

   929  *** insert: preserved ["IsacKnowledge","Rational","Rulesets","norm_Rational"]

   930  *** insert: preserved ["IsacKnowledge","Rational","Rulesets","norm_Rational_rls"]

   931  *** insert: preserved ["IsacKnowledge","Rational","Rulesets","norm_Rational_parenthesized"]

   932  *** insert: preserved ["IsacKnowledge","Rational","Rulesets","rat_mult_poly"]

   933  *** insert: preserved ["IsacKnowledge","Rational","Rulesets","rat_mult_div_pow"]

   934  *** insert: preserved ["IsacKnowledge","Rational","Rulesets","cancel_p_rls"]

   935  *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_pow"]

   936  *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_addI"]

   937  *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_oneI"]

   938  *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_twoI"]

   939  *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_multI"]

   940  *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_zeroI"]

   941  *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_diff_plus"]

   942  *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_plus_1"]

   943  *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_diff_minus"]

   944  *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_eq_oneI"]

   945  *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_num_collect"]

   946  *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_one_collect"]

   947  *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_def_atom"]

   948  *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_two_atom"]

   949  *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_mult_2_assoc"]

   950  *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_addI_atom"]

   951  *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_minus_odd"]

   952  *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_minus_even"]

   953  *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_minus_oneI"]

   954  *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_multI_poly"]

   955  *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_mm_binom_times"]

   956  *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_mp_binom_times"]

   957  *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_mult_2_assoc_l"]

   958  *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_mult_2_assoc_r"]

   959  *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_pm_binom_times"]

   960  *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_pp_binom_times"]

   961  *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_plus_1_atom"]

   962  *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_binom_pow2"]

   963  *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_binom_pow3"]

   964  *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_binom_pow4"]

   965  *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_binom_pow5"]

   966  *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_addI_assoc_l"]

   967  *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_addI_assoc_r"]

   968  *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_twoI_assoc_l"]

   969  *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_twoI_assoc_r"]

   970  *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_minus_binom_pow2"]

   971  *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_minus_binom_pow3"]

   972  *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_binom_times"]

   973  *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_minus_binom_times"]

   974  *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_num_collect_assoc"]

   975  *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_one_collect_assoc"]

   976  *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_binom_times1"]

   977  *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_binom_times2"]

   978  *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_minus_binom1"]

   979  *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_minus_binom2"]

   980  *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_plus_1_assoc_l"]

   981  *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_plus_1_assoc_r"]

   982  *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_minus_binom_pow2_p"]

   983  *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_minus_binom_pow3_p"]

   984  *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_plus_1_assoc_l2"]

   985  *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_num_collect_assoc_l"]

   986  *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_num_collect_assoc_r"]

   987  *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_one_collect_assoc_l"]

   988  *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_one_collect_assoc_r"]

   989  *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_minus_binom1_p"]

   990  *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_minus_binom2_p"]

   991  *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_binom_pow2_poly"]

   992  *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_binom_pow3_poly"]

   993  *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_binom_pow4_poly"]

   994  *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_binom_pow5_poly"]

   995  *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_add_mult_distrib_poly"]

   996  *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_minus_binom1_p_p"]

   997  *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_minus_binom2_p_p"]

   998  *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_add_mult_distrib2_poly"]

   999  *** insert: preserved ["IsacKnowledge","Poly","Rulesets","norm_Poly"]

  1000  *** insert: preserved ["IsacKnowledge","Poly","Rulesets","Poly_erls"]

  1001  *** insert: preserved ["IsacKnowledge","Poly","Rulesets","expand"]

  1002  *** insert: preserved ["IsacKnowledge","Poly","Rulesets","expand_poly"]

  1003  *** insert: preserved ["IsacKnowledge","Poly","Rulesets","simplify_power"]

  1004  *** insert: preserved ["IsacKnowledge","Poly","Rulesets","order_add_mult"]

  1005  *** insert: preserved ["IsacKnowledge","Poly","Rulesets","collect_numerals"]

  1006  *** insert: preserved ["IsacKnowledge","Poly","Rulesets","collect_numerals_"]

  1007  *** insert: preserved ["IsacKnowledge","Poly","Rulesets","reduce_012"]

  1008  *** insert: preserved ["IsacKnowledge","Poly","Rulesets","discard_parentheses"]

  1009  *** insert: preserved ["IsacKnowledge","Poly","Rulesets","make_polynomial"]

  1010  *** insert: preserved ["IsacKnowledge","Poly","Rulesets","expand_binoms"]

  1011  *** insert: preserved ["IsacKnowledge","Poly","Rulesets","rev_rew_p"]

  1012  *** insert: preserved ["IsacKnowledge","Poly","Rulesets","expand_poly_"]

  1013  *** insert: preserved ["IsacKnowledge","Poly","Rulesets","expand_poly_rat_"]

  1014  *** insert: preserved ["IsacKnowledge","Poly","Rulesets","simplify_power_"]

  1015  *** insert: preserved ["IsacKnowledge","Poly","Rulesets","calc_add_mult_pow_"]

  1016  *** insert: preserved ["IsacKnowledge","Poly","Rulesets","reduce_012_mult_"]

  1017  *** insert: preserved ["IsacKnowledge","Poly","Rulesets","reduce_012_"]

  1018  *** insert: preserved ["IsacKnowledge","Poly","Rulesets","discard_parentheses1"]

  1019  *** insert: preserved ["IsacKnowledge","Poly","Rulesets","order_mult_rls_"]

  1020  *** insert: preserved ["IsacKnowledge","Poly","Rulesets","order_add_rls_"]

  1021  *** insert: preserved ["IsacKnowledge","Poly","Rulesets","make_rat_poly_with_parentheses"]

  1022  *** insert: preserved ["IsacKnowledge","Atools","Theorems","or_true"]

  1023  *** insert: preserved ["IsacKnowledge","Atools","Theorems","and_true"]

  1024  *** insert: preserved ["IsacKnowledge","Atools","Theorems","not_true"]

  1025  *** insert: preserved ["IsacKnowledge","Atools","Theorems","or_false"]

  1026  *** insert: preserved ["IsacKnowledge","Atools","Theorems","rat_leq1"]

  1027  *** insert: preserved ["IsacKnowledge","Atools","Theorems","rat_leq2"]

  1028  *** insert: preserved ["IsacKnowledge","Atools","Theorems","rat_leq3"]

  1029  *** insert: preserved ["IsacKnowledge","Atools","Theorems","rle_refl"]

  1030  *** insert: preserved ["IsacKnowledge","Atools","Theorems","and_false"]

  1031  *** insert: preserved ["IsacKnowledge","Atools","Theorems","last_thmI"]

  1032  *** insert: preserved ["IsacKnowledge","Atools","Theorems","not_false"]

  1033  *** insert: preserved ["IsacKnowledge","Atools","Theorems","or_commute"]

  1034  *** insert: preserved ["IsacKnowledge","Atools","Theorems","and_commute"]

  1035  *** insert: preserved ["IsacKnowledge","Atools","Theorems","real_unari_minus"]

  1036  *** insert: preserved ["IsacKnowledge","Atools","Theorems","radd_left_cancel_le"]

  1037  *** insert: preserved ["IsacKnowledge","Delete","Theorems","real_diff_0"]

  1038  *** insert: preserved ["IsacKnowledge","Delete","Theorems","real_mult_2"]

  1039  *** insert: preserved ["IsacKnowledge","Delete","Theorems","real_mult_minus1"]

  1040  *** insert: preserved ["IsacKnowledge","Delete","Theorems","real_mult_left_commute"]

  1041  *** insert: preserved ["IsacKnowledge","Script","Theorems","arity_type_ID"]

  1042  *** insert: preserved ["IsacKnowledge","Script","Theorems","arity_type_arg"]

  1043  *** insert: preserved ["IsacKnowledge","Tools","Theorems","arity_type_cpy"]

  1044  *** insert: preserved ["IsacKnowledge","Tools","Theorems","arity_type_nam"]

  1045  *** insert: preserved ["IsacKnowledge","Tools","Theorems","arity_type_str"]

  1046  *** insert: preserved ["IsacKnowledge","Tools","Theorems","arity_type_una"]

  1047  *** insert: preserved ["IsacKnowledge","Tools","Theorems","arity_type_unl"]

  1048  *** insert: preserved ["IsacKnowledge","Tools","Theorems","arity_type_toreal"]

  1049  *** insert: preserved ["IsacKnowledge","Tools","Theorems","arity_type_unknow"]

  1050  *** insert: preserved ["IsacKnowledge","Tools","Theorems","arity_type_tobooll"]

  1051  *** insert: preserved ["IsacKnowledge","Tools","Theorems","arity_type_toreall"]

  1052  *** insert: preserved ["IsacKnowledge","Tools","Rulesets","e_rls"]

  1053  *** insert: preserved ["IsacKnowledge","Tools","Rulesets","e_rrls"]

  1054  *** insert: preserved ["IsacKnowledge","ListC","Theorems","LAST"]  = ["IsacScripts","ListC"---\

  1055  *** insert: preserved ["IsacKnowledge","ListC","Theorems","hd_thm"]

  1056  *** insert: preserved ["IsacKnowledge","ListC","Theorems","tl_Nil"]

  1057  *** insert: preserved ["IsacKnowledge","ListC","Theorems","NTH_NIL"]

  1058  *** insert: preserved ["IsacKnowledge","ListC","Theorems","del_def"]

  1059  *** insert: preserved ["IsacKnowledge","ListC","Theorems","map_Nil"]

  1060  *** insert: preserved ["IsacKnowledge","ListC","Theorems","mem_Nil"]

  1061  *** insert: preserved ["IsacKnowledge","ListC","Theorems","rev_Nil"]

  1062  *** insert: preserved ["IsacKnowledge","ListC","Theorems","tl_Cons"]

  1063  *** insert: preserved ["IsacKnowledge","ListC","Theorems","zip_Nil"]

  1064  *** insert: preserved ["IsacKnowledge","ListC","Theorems","NTH_CONS"]

  1065  *** insert: preserved ["IsacKnowledge","ListC","Theorems","map_Cons"]

  1066  *** insert: preserved ["IsacKnowledge","ListC","Theorems","mem_Cons"]

  1067  *** insert: preserved ["IsacKnowledge","ListC","Theorems","null_Nil"]

  1068  *** insert: preserved ["IsacKnowledge","ListC","Theorems","rev_Cons"]

  1069  *** insert: preserved ["IsacKnowledge","ListC","Theorems","zip_Cons"]

  1070  *** insert: preserved ["IsacKnowledge","ListC","Theorems","foldr_Nil"]

  1071  *** insert: preserved ["IsacKnowledge","ListC","Theorems","null_Cons"]

  1072  *** insert: preserved ["IsacKnowledge","ListC","Theorems","LENGTH_def"]

  1073  *** insert: preserved ["IsacKnowledge","ListC","Theorems","append_Nil"]

  1074  *** insert: preserved ["IsacKnowledge","ListC","Theorems","concat_Nil"]

  1075  *** insert: preserved ["IsacKnowledge","ListC","Theorems","filter_Nil"]

  1076  *** insert: preserved ["IsacKnowledge","ListC","Theorems","foldr_Cons"]

  1077  *** insert: preserved ["IsacKnowledge","ListC","Theorems","append_Cons"]

  1078  *** insert: preserved ["IsacKnowledge","ListC","Theorems","butlast_Nil"]

  1079  *** insert: preserved ["IsacKnowledge","ListC","Theorems","concat_Cons"]

  1080  *** insert: preserved ["IsacKnowledge","ListC","Theorems","filter_Cons"]

  1081  *** insert: preserved ["IsacKnowledge","ListC","Theorems","remdups_Nil"]

  1082  *** insert: preserved ["IsacKnowledge","ListC","Theorems","butlast_Cons"]

  1083  *** insert: preserved ["IsacKnowledge","ListC","Theorems","distinct_Nil"]

  1084  *** insert: preserved ["IsacKnowledge","ListC","Theorems","remdups_Cons"]

  1085  *** insert: preserved ["IsacKnowledge","ListC","Theorems","distinct_Cons"]

  1086  *** insert: preserved ["IsacKnowledge","ListC","Theorems","dropWhile_Nil"]

  1087  *** insert: preserved ["IsacKnowledge","ListC","Theorems","takeWhile_Nil"]

  1088  *** insert: preserved ["IsacKnowledge","ListC","Theorems","dropWhile_Cons"]

  1089  *** insert: preserved ["IsacKnowledge","ListC","Theorems","takeWhile_Cons"]

  1090  *** insert: preserved ["IsacKnowledge","ListC","Theorems","list_diff_def_raw"]=["IsacScripts"---/

  1091  val it = (): unit

  1093 *)

  1095 "-------- retrieve errpats ------------------------------";

  1096 "-------- retrieve errpats ------------------------------";

  1097 "-------- retrieve errpats ------------------------------";

  1098 val {errpats, nrls, scr = Prog prog, ...} = get_met ["diff", "differentiate_on_R"];

  1099 case errpats of [("chain-rule-diff-both", _, _)] => ()

  1100   | _ => error "errpats chain-rule-diff-both changed"

author	Walther Neuper <neuper@ist.tugraz.at>
	Mon, 16 Sep 2013 12:20:00 +0200
changeset 52105	2786cc9704c8
parent 52062	b3f18f0d55d9
child 52148	aabc6c8e930a
permissions	-rw-r--r--