WN130922 Build_Thydata.thy:

   writeln "======= begin ! ruleset' =======";

   ! ruleset' |> rev (*!!!!!*) 

     |> map check_kestore_rls |> map writeln;

   writeln "======= ! ruleset' ordered =======";

 --------------------------------------------------------------------------------------

 ======= length (! ruleset')   = 124

 --------------------------------------------------------------------------------------

 ======= begin ! ruleset' =======

 (expand_binomtest, (Test, Rls {#calc = 3, #rules = 29, ...))

 (make_polytest, (Test, Rls {#calc = 3, #rules = 25, ...))

 (rearrange_assoc, (Test, Rls {#calc = 0, #rules = 2, ...))

 (ac_plus_times, (Test, Rls {#calc = 0, #rules = 6, ...))

 (norm_equation, (Test, Rls {#calc = 0, #rules = 1, ...))

 (inverse_z, (Inverse_Z_Transform, Rls {#calc = 0, #rules = 1, ...))

 (matches, (Test, Rls {#calc = 8, #rules = 20, ...))

 (isolate_bdv, (Test, Rls {#calc = 0, #rules = 6, ...))

 (isolate_root, (Test, Rls {#calc = 0, #rules = 6, ...))

 (tval_rls, (Test, Rls {#calc = 11, #rules = 27, ...))

 (Test_simplify, (Test, Rls {#calc = 4, #rules = 37, ...))

 (testerls, (Test, Rls {#calc = 8, #rules = 19, ...))

 (norm_System, (EqSystem, Rls {#calc = 0, #rules = 9, ...))

 (norm_System_noadd_fractions, (EqSystem, Rls {#calc = 0, #rules = 8, ...))

 (order_add_mult_System, (EqSystem, Rls {#calc = 0, #rules = 6, ...))

 (order_system, (EqSystem, Rls {#calc = 0, #rules = 1, ...))

 (isolate_bdvs_4x4, (EqSystem, Rls {#calc = 0, #rules = 5, ...))

 (isolate_bdvs, (EqSystem, Rls {#calc = 0, #rules = 3, ...))

 (simplify_System, (EqSystem, Seq {#calc = 1, #rules = 6, ...))

 (simplify_System_parenthesized, (EqSystem, Seq {#calc = 1, #rules = 8, ...))

 ----- ruleset.Unsynchronized-1: (testerls, (Test, Rls {#calc = 8, #rules = 19, ...))

 (norm_Rational_rls_noadd_fractions, (Integrate, Rls {#calc = 0, #rules = 4, ...))

 (norm_Rational_noadd_fractions, (Integrate, Seq {#calc = 0, #rules = 6, ...))

 (separate_bdv2, (Integrate, Rls {#calc = 0, #rules = 22, ...))

 (integration, (Integrate, Seq {#calc = 0, #rules = 3, ...))

 (simplify_Integral, (Integrate, Seq {#calc = 1, #rules = 7, ...))

 (add_new_c, (Integrate, Seq {#calc = 0, #rules = 1, ...))

 (integration_rules, (Integrate, Rls {#calc = 1, #rules = 6, ...))

 (eval_rls, (DiffApp, Rls {#calc = 0, #rules = 19, ...))

 (diff_sym_conv, (Diff, Rls {#calc = 1, #rules = 8, ...))

 (diff_conv, (Diff, Rls {#calc = 1, #rules = 10, ...))

 (norm_diff, (Diff, Rls {#calc = 0, #rules = 2, ...))

 (diff_rules, (Diff, Rls {#calc = 0, #rules = 2, ...))

 (separate_bdvs, (PolyEq, Rls {#calc = 0, #rules = 23, ...))

 (make_ratpoly_in, (PolyEq, Seq {#calc = 0, #rules = 5, ...))

 (make_polynomial_in, (PolyEq, Seq {#calc = 0, #rules = 8, ...))

 (collect_bdv, (PolyEq, Rls {#calc = 0, #rules = 18, ...))

 (order_add_mult_in, (PolyEq, Rls {#calc = 0, #rules = 6, ...))

 (d4_polyeq_simplify, (PolyEq, Rls {#calc = 0, #rules = 1, ...))

 (d3_polyeq_simplify, (PolyEq, Rls {#calc = 0, #rules = 21, ...))

 (d2_polyeq_abcFormula_simplify, (PolyEq, Rls {#calc = 0, #rules = 18, ...))

 (d2_polyeq_pqFormula_simplify, (PolyEq, Rls {#calc = 0, #rules = 18, ...))

 (d2_polyeq_sq_only_simplify, (PolyEq, Rls {#calc = 0, #rules = 6, ...))

 (d2_polyeq_bdv_only_simplify, (PolyEq, Rls {#calc = 0, #rules = 10, ...))

 (d2_polyeq_simplify, (PolyEq, Rls {#calc = 0, #rules = 24, ...))

 (d1_polyeq_simplify, (PolyEq, Rls {#calc = 0, #rules = 3, ...))

 (d0_polyeq_simplify, (PolyEq, Rls {#calc = 0, #rules = 2, ...))

 (polyeq_simplify, (PolyEq, Rls {#calc = 6, #rules = 12, ...))

 (PolyEq_erls, (PolyEq, Rls {#calc = 1, #rules = 42, ...))

 (complete_square, (PolyEq, Rls {#calc = 0, #rules = 5, ...))

 (cancel_leading_coeff, (PolyEq, Rls {#calc = 0, #rules = 13, ...))

 (equival_trans, (Partial_Fractions, Rls {#calc = 0, #rules = 2, ...))

 (multiply_ansatz, (Partial_Fractions, Rls {#calc = 0, #rules = 1, ...))

 (ansatz_rls, (Partial_Fractions, Rls {#calc = 0, #rules = 2, ...))

 (rootrat_solve, (RootRatEq, Rls {#calc = 0, #rules = 4, ...))

 (RooRatEq_erls, (RootRatEq, Rls {#calc = 2, #rules = 43, ...))

 (klammern_ausmultiplizieren, (PolyMinus, Rls {#calc = 0, #rules = 4, ...))

 (klammern_aufloesen, (PolyMinus, Rls {#calc = 0, #rules = 4, ...))

 (ordne_monome, (PolyMinus, Rls {#calc = 0, #rules = 4, ...))

 (verschoenere, (PolyMinus, Rls {#calc = 1, #rules = 10, ...))

 (fasse_zusammen, (PolyMinus, Rls {#calc = 2, #rules = 24, ...))

 (ordne_alphabetisch, (PolyMinus, Rls {#calc = 0, #rules = 8, ...))

 (calculate_RootRat, (RootRat, Rls {#calc = 2, #rules = 19, ...))

 (rootrat_erls, (RootRat, Rls {#calc = 14, #rules = 41, ...))

 (RatEq_simplify, (RatEq, Rls {#calc = 0, #rules = 8, ...))

 (RatEq_eliminate, (RatEq, Rls {#calc = 0, #rules = 3, ...))

 (rateq_erls, (RatEq, Rls {#calc = 1, #rules = 41, ...))

 (rooteq_simplify, (RootEq, Rls {#calc = 6, #rules = 15, ...))

 (r_sqrt_isolate, (RootEq, Rls {#calc = 0, #rules = 16, ...))

 (l_sqrt_isolate, (RootEq, Rls {#calc = 0, #rules = 16, ...))

 (sqrt_isolate, (RootEq, Rls {#calc = 0, #rules = 32, ...))

 (rooteq_srls, (RootEq, Rls {#calc = 0, #rules = 3, ...))

 (RootEq_erls, (RootEq, Rls {#calc = 0, #rules = 28, ...))

 (cancel_p_rls, (Rational, Rls {#calc = 0, #rules = 1, ...))

 (rat_mult_div_pow, (Rational, Rls {#calc = 1, #rules = 8, ...))

 (rat_mult_poly, (Rational, Rls {#calc = 0, #rules = 2, ...))

 (norm_Rational_parenthesized, (Rational, Seq {#calc = 0, #rules = 2, ...))

 (norm_Rational_rls, (Rational, Rls {#calc = 0, #rules = 5, ...))

 (norm_Rational, (Rational, Seq {#calc = 0, #rules = 6, ...))

 (norm_rat_erls, (Rational, Rls {#calc = 1, #rules = 1, ...))

 (rat_reduce_1, (Rational, Rls {#calc = 0, #rules = 2, ...))

 (reduce_0_1_2, (Rational, Rls {#calc = 0, #rules = 6, ...))

 (rat_mult_divide, (Rational, Rls {#calc = 1, #rules = 6, ...))

 (powers, (Rational, Rls {#calc = 1, #rules = 11, ...))

 (powers_erls, (Rational, Rls {#calc = 4, #rules = 6, ...))

 (add_fractions_p_rls, (Rational, Rls {#calc = 0, #rules = 1, ...))

 (add_fractions_p, (Rational, Rrls {...}))

 (cancel_p, (Rational, Rrls {...}))

 (rational_erls, (Rational, Rls {#calc = 1, #rules = 35, ...))

 (calc_rat_erls, (Rational, Rls {#calc = 2, #rules = 4, ...))

 (calculate_Rational, (Rational, Rls {#calc = 1, #rules = 15, ...))

 (LinEq_simplify, (LinEq, Rls {#calc = 0, #rules = 3, ...))

 (LinPoly_simplify, (LinEq, Rls {#calc = 4, #rules = 5, ...))

 (LinEq_erls, (LinEq, Rls {#calc = 0, #rules = 26, ...))

 (expand_rootbinoms, (Root, Rls {#calc = 6, #rules = 33, ...))

 (make_rooteq, (Root, Rls {#calc = 3, #rules = 25, ...))

 (Root_erls, (Root, Rls {#calc = 0, #rules = 27, ...))

 (make_rat_poly_with_parentheses, (Poly, Seq {#calc = 1, #rules = 10, ...))

 (order_add_rls_, (Poly, Rls {#calc = 0, #rules = 1, ...))

 (order_mult_rls_, (Poly, Rls {#calc = 0, #rules = 1, ...))

 (discard_parentheses1, (Poly, Rls {#calc = 0, #rules = 1, ...))

 (reduce_012_, (Poly, Rls {#calc = 0, #rules = 6, ...))

 (reduce_012_mult_, (Poly, Rls {#calc = 0, #rules = 4, ...))

 (calc_add_mult_pow_, (Poly, Rls {#calc = 3, #rules = 3, ...))

 (simplify_power_, (Poly, Rls {#calc = 0, #rules = 8, ...))

 (expand_poly_rat_, (Poly, Rls {#calc = 0, #rules = 10, ...))

 (expand_poly_, (Poly, Rls {#calc = 0, #rules = 8, ...))

 (discard_minus, (Poly, Rls {#calc = 0, #rules = 2, ...))

 (rev_rew_p, (Poly, Seq {#calc = 3, #rules = 25, ...))

 (expand_binoms, (Poly, Rls {#calc = 3, #rules = 29, ...))

 (make_polynomial, (Poly, Seq {#calc = 1, #rules = 11, ...))

 (discard_parentheses, (Poly, Rls {#calc = 0, #rules = 2, ...))

 (reduce_012, (Poly, Rls {#calc = 0, #rules = 7, ...))

 (collect_numerals_, (Poly, Rls {#calc = 1, #rules = 7, ...))

 (collect_numerals, (Poly, Rls {#calc = 3, #rules = 7, ...))

 (order_add_mult, (Poly, Rls {#calc = 0, #rules = 6, ...))

 (simplify_power, (Poly, Rls {#calc = 0, #rules = 7, ...))

 (expand_poly, (Poly, Rls {#calc = 0, #rules = 9, ...))

 (expand, (Poly, Rls {#calc = 0, #rules = 2, ...))

 (Poly_erls, (Poly, Rls {#calc = 0, #rules = 25, ...))

 (norm_Poly, (Poly, Seq {#calc = 1, #rules = 11, ...))

 (univariate_equation_prls, (Equation, Rls {#calc = 1, #rules = 1, ...))

 (list_rls, (DiffApp, Rls {#calc = 8, #rules = 53, ...))

 (e_rrls, (Tools, Rrls {...}))

 (e_rls, (Tools, Rls {#calc = 0, #rules = 0, ...))

 ======= ! ruleset' ordered =======