src/Tools/isac/Knowledge/LogExp.thy
branchisac-update-Isa09-2
changeset 37991 028442673981
parent 37983 03bfbc480107
child 37992 351a9e94c38d
     1.1 --- a/src/Tools/isac/Knowledge/LogExp.thy	Wed Sep 08 16:45:27 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/LogExp.thy	Wed Sep 08 16:47:22 2010 +0200
     1.3 @@ -32,10 +32,10 @@
     1.4   (prep_pbt thy "pbl_test_equ_univ_log" [] e_pblID
     1.5   (["logarithmic","univariate","equation"],
     1.6    [("#Given",["equality e_e","solveFor v_v"]),
     1.7 -   ("#Where",["matches ((?a log ?v_) = ?b) e_e"]),
     1.8 +   ("#Where",["matches ((?a log ?v_v) = ?b) e_e"]),
     1.9     ("#Find" ,["solutions v_i"]),
    1.10 -   ("#With" ,["||(lhs (Subst (v_i_,v_) e_e) - " ^
    1.11 -	      "  (rhs (Subst (v_i_,v_) e_e) || < eps)"])
    1.12 +   ("#With" ,["||(lhs (Subst (v_i_,v_v) e_e) - " ^
    1.13 +	      "  (rhs (Subst (v_i_,v_v) e_e) || < eps)"])
    1.14     ],
    1.15    PolyEq_prls, SOME "solve (e_e::bool, v_v)",
    1.16    [["Equation","solve_log"]]));
    1.17 @@ -45,7 +45,7 @@
    1.18   (prep_met thy "met_equ_log" [] e_metID
    1.19   (["Equation","solve_log"],
    1.20    [("#Given" ,["equality e_e","solveFor v_v"]),
    1.21 -   ("#Where" ,["matches ((?a log ?v_) = ?b) e_e"]),
    1.22 +   ("#Where" ,["matches ((?a log ?v_v) = ?b) e_e"]),
    1.23     ("#Find"  ,["solutions v_i"])
    1.24    ],
    1.25     {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls,