1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml	Tue Sep 20 18:09:46 2011 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml	Thu Sep 22 14:24:34 2011 +0200
     1.3 @@ -26,7 +26,6 @@
     1.4  "----------- pbl binom polynom vereinfachen: cube -------";
     1.5  "----------- refine Vereinfache -------------------------";
     1.6  "----------- *** prep_pbt: syntax error in '#Where' of [v";
     1.7 -"----------- check: fmz matches pbt ---------------------";
     1.8  "--------------------------------------------------------";
     1.9  "--------------------------------------------------------";
    1.10  "--------------------------------------------------------";
    1.11 @@ -641,30 +640,6 @@
    1.12  then () else error "polyminus.sml type-structure of \"?a :: real\" changed 1";
    1.13  show_types := false;
    1.14  
    1.15 -"----------- check: fmz matches pbt ---------------------";
    1.16 -"----------- check: fmz matches pbt ---------------------";
    1.17 -"----------- check: fmz matches pbt ---------------------";
    1.18 -"101230 error *** nxt_add: EX itm. not(dat(itm)<=dat(ori))";
    1.19 -val fmz = ["TERM (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)","normalform N"];
    1.20 -val pI = ["plus_minus","polynom","vereinfachen"];
    1.21 -prep_ori fmz thy ((#ppc o get_pbt) pI);
    1.22 -(*val it =
    1.23 -   [(1, [1], "#undef", Const (...), [...]),       <<<===
    1.24 -    (2, [1], "#Find", Const (...), [...])]
    1.25 -   : ori list
    1.26 -*)
    1.27 -val t = str2term "TERM ttt";
    1.28 -atomwy t;
    1.29 -val t = str2term "term ttt";
    1.30 -atomwy t;
    1.31 -val t = str2term "Term ttt";
    1.32 -atomwy t;
    1.33 -val fmz = ["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)","normalform N"];
    1.34 -prep_ori fmz thy ((#ppc o get_pbt) pI);
    1.35 -(*val it =
    1.36 -   [(1, [1], "#Given", Const (...), [...]),
    1.37 -    (2, [1], "#Find", Const (...), [...])]
    1.38 -   : ori list
    1.39 -*)
    1.40 +
    1.41  ============ inhibit exn 110719 ==============================================*)
    1.42