1.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy	Mon Jan 27 21:58:57 2014 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy	Mon Jan 27 22:26:51 2014 +0100
     1.3 @@ -168,19 +168,6 @@
     1.4  
     1.5  ML {*
     1.6  check_guhs_unique := false; (*WN120307 REMOVE after editing*)
     1.7 -store_pbt
     1.8 - (prep_pbt @{theory} "pbl_simp_rat_partfrac" [] e_pblID
     1.9 - (["partial_fraction", "rational", "simplification"],
    1.10 -  [("#Given" ,["functionTerm t_t", "solveFor v_v"]),
    1.11 -   (* TODO: call this sub-problem with appropriate functionTerm: 
    1.12 -      leading coefficient of the denominator is 1: to be checked here! and..
    1.13 -     ("#Where" ,["((get_numerator t_t) has_degree_in v_v) < 
    1.14 -                  ((get_denominator t_t) has_degree_in v_v)"]), TODO*)
    1.15 -   ("#Find"  ,["decomposedFunction p_p'''"])
    1.16 -  ],
    1.17 -  append_rls "e_rls" e_rls [(*for preds in where_ TODO*)], 
    1.18 -  NONE, 
    1.19 -  [["simplification","of_rationals","to_partial_fraction"]]));
    1.20  *}
    1.21  setup {* KEStore_Elems.add_pbts
    1.22    [(prep_pbt @{theory} "pbl_simp_rat_partfrac" [] e_pblID