1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Mon Jan 27 21:58:57 2014 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Mon Jan 27 22:26:51 2014 +0100
     1.3 @@ -117,29 +117,9 @@
     1.4  *}
     1.5  setup {* KEStore_Elems.add_rlss 
     1.6    [("LinEq_simplify", (Context.theory_name @{theory}, LinEq_simplify))] *}
     1.7 -ML {*
     1.8  
     1.9  (*----------------------------- problem types --------------------------------*)
    1.10 -(* 
    1.11 -show_ptyps(); 
    1.12 -(get_pbt ["LINEAR","univariate","equation"]);
    1.13 -*)
    1.14 -
    1.15  (* ---------linear----------- *)
    1.16 -store_pbt
    1.17 - (prep_pbt thy "pbl_equ_univ_lin" [] e_pblID
    1.18 - (["LINEAR","univariate","equation"],
    1.19 -  [("#Given" ,["equality e_e","solveFor v_v"]),
    1.20 -   ("#Where" ,["HOL.False", (*WN0509 just detected: this pbl can never be used?!?*)
    1.21 -               "Not( (lhs e_e) is_polyrat_in v_v)",
    1.22 -               "Not( (rhs e_e) is_polyrat_in v_v)",
    1.23 -               "((lhs e_e) has_degree_in v_v)=1",
    1.24 -	       "((rhs e_e) has_degree_in v_v)=1"]),
    1.25 -   ("#Find"  ,["solutions v_v'i'"]) 
    1.26 -  ],
    1.27 -  LinEq_prls, SOME "solve (e_e::bool, v_v)",
    1.28 -  [["LinEq","solve_lineq_equation"]]));
    1.29 -*}
    1.30  setup {* KEStore_Elems.add_pbts
    1.31    [(prep_pbt thy "pbl_equ_univ_lin" [] e_pblID
    1.32        (["LINEAR", "univariate", "equation"],