src/Tools/isac/Knowledge/LinEq.thy
changeset 55276 ce872d7781d2
parent 52155 e4ddf21390fd
child 55339 cccd24e959ba
     1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Thu Nov 21 11:17:42 2013 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Thu Nov 21 11:46:00 2013 +0100
     1.3 @@ -122,13 +122,13 @@
     1.4  (*----------------------------- problem types --------------------------------*)
     1.5  (* 
     1.6  show_ptyps(); 
     1.7 -(get_pbt ["linear","univariate","equation"]);
     1.8 +(get_pbt ["LINEAR","univariate","equation"]);
     1.9  *)
    1.10  
    1.11  (* ---------linear----------- *)
    1.12  store_pbt
    1.13   (prep_pbt thy "pbl_equ_univ_lin" [] e_pblID
    1.14 - (["linear","univariate","equation"],
    1.15 + (["LINEAR","univariate","equation"],
    1.16    [("#Given" ,["equality e_e","solveFor v_v"]),
    1.17     ("#Where" ,["HOL.False", (*WN0509 just detected: this pbl can never be used?!?*)
    1.18                 "Not( (lhs e_e) is_polyrat_in v_v)",