1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Mon Jan 20 16:15:34 2014 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Tue Jan 21 00:27:44 2014 +0100
     1.3 @@ -139,7 +139,20 @@
     1.4    ],
     1.5    LinEq_prls, SOME "solve (e_e::bool, v_v)",
     1.6    [["LinEq","solve_lineq_equation"]]));
     1.7 +*}
     1.8 +setup {* KEStore_Elems.store_pbts
     1.9 +  [(prep_pbt thy "pbl_equ_univ_lin" [] e_pblID
    1.10 +      (["LINEAR", "univariate", "equation"],
    1.11 +        [("#Given" ,["equality e_e", "solveFor v_v"]),
    1.12 +          ("#Where" ,["HOL.False", (*WN0509 just detected: this pbl can never be used?!?*)
    1.13 +              "Not( (lhs e_e) is_polyrat_in v_v)",
    1.14 +              "Not( (rhs e_e) is_polyrat_in v_v)",
    1.15 +              "((lhs e_e) has_degree_in v_v)=1",
    1.16 +	            "((rhs e_e) has_degree_in v_v)=1"]),
    1.17 +          ("#Find"  ,["solutions v_v'i'"])],
    1.18 +        LinEq_prls, SOME "solve (e_e::bool, v_v)", [["LinEq", "solve_lineq_equation"]]))] *}
    1.19  
    1.20 +ML {*
    1.21  (*-------------- methods------------------------------------------------------*)
    1.22  store_met
    1.23   (prep_met thy "met_eqlin" [] e_metID