(* all outcommented in order to demonstrate authoring:

    WN071203

 *)

 (** interface isabelle -- isac **)

 theory' := overwritel (!theory', [("LogExp.thy",LogExp.thy)]);

 (*--------------------------------------------------*)

 (** problems **)

 store_pbt

  (prep_pbt LogExp.thy "pbl_test_equ_univ_log" [] e_pblID

  (["logarithmic","univariate","equation"],

   [("#Given",["equality e_","solveFor v_"]),

    ("#Where",["matches ((?a log ?v_) = ?b) e_"]),

    ("#Find" ,["solutions v_i_"]),

    ("#With" ,["||(lhs (Subst (v_i_,v_) e_) - \

 	      \  (rhs (Subst (v_i_,v_) e_) || < eps)"])

    ],

   PolyEq_prls, Some "solve (e_::bool, v_)",

   [["Equation","solve_log"]]));

 (** methods **)

 store_met

  (prep_met LogExp.thy "met_equ_log" [] e_metID

  (["Equation","solve_log"],

   [("#Given" ,["equality e_","solveFor v_"]),

    ("#Where" ,["matches ((?a log ?v_) = ?b) e_"]),

    ("#Find"  ,["solutions v_i_"])

   ],

    {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls,

     calc=[],crls=PolyEq_crls, nrls=norm_Rational},

     "Script Solve_log (e_::bool) (v_::real) =     \

     \(let e_ = ((Rewrite equality_power False) @@ \

     \           (Rewrite exp_invers_log False) @@ \

     \           (Rewrite_Set norm_Poly False)) e_ \

     \ in [e_])"

    ));

 (*--------------------------------------------------*)