###  rls: e_rls on: x ~= 0 

  ###  rls: e_rls on: x ~= 0 

  ##  asms accepted: ["x ~= 0"]   stored: ["x ~= 0"] 

  ##  asms accepted: ["x ~= 0"]   stored: ["x ~= 0"] 

 *)

 *)

 trace_rewrite := false;

 trace_rewrite := false;

 val SOME (t', []) = rewrite_set_ thy true RatEq_eliminate t; (*= [] must be = "x ~= 0"*)

 val SOME (t', []) = rewrite_set_ thy true RatEq_eliminate t; (*= [] must be = "x ~= 0"*)

 term2str t' = "1 = 5 * x";

 term2str t' = "1 = 5 * x";

 (*

 (*

  :

  :

  ####  rls: rateq_erls on: x ~= 0 

  ####  rls: rateq_erls on: x ~= 0