wneuper/isac: src/sml/IsacKnowledge/LogExp.ML@a99ad24f209f

     1 (* all outcommented in order to demonstrate authoring:

     2    WN071203

     3 *)

     5 (** interface isabelle -- isac **)

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

     8 (*-------------------------------------------------------------------*

    10 (** problems **)

    11 store_pbt

    12  (prep_pbt LogExp.thy "pbl_test_equ_univ_log" [] e_pblID

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

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

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

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

    17    ],

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

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

    21 (** methods **)

    22 store_met

    23  (prep_met LogExp.thy "met_equ_log" [] e_metID

    24  (["Equation","solve_log"],

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

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

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

    28   ],

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

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

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

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

    33     \           (Rewrite exp_invers_log False) @@ \

    34     \           (Rewrite_Set norm_Poly False)) e_ \

    35     \ in [e_])"

    36    ));

    37 *-------------------------------------------------------------------*)

author	wneuper
	Mon, 03 Dec 2007 19:45:05 +0100
branch	start-work-070517
changeset 258	a99ad24f209f
parent 257	92038d7dfe6b
permissions	-rw-r--r--