ruleset.Unsynchronized-1 and ruleset.Unsynchronized-2 are copies from ~/.isabelle/../log/Isac,

 where log/Isac was created by two different session Isac. and the output stems from ...

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

 Build_Thydata.thy:

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

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

     |> map check_kestore_rls |> map writeln;

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

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

 ======= 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, ...))

 ----- ruleset.Unsynchronized-2: (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, ...))

 ----- ruleset.Unsynchronized-2: (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, ...))

 (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, ...))

 :

 :

 :

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