test/Tools/isac/Knowledge/polyminus.sml
branchdecompose-isar
changeset 42098 c77e77ebbf3d
parent 42017 ce19769e9dc4
child 42102 8a263c47ac85
     1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml	Mon Jul 18 09:50:15 2011 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml	Mon Jul 18 15:20:04 2011 +0200
     1.3 @@ -37,7 +37,6 @@
     1.4  "----------- fun eval_ist_monom ----------------------------------";
     1.5  "----------- fun eval_ist_monom ----------------------------------";
     1.6  ist_monom (str2term "12");
     1.7 -(*========== inhibit exn =======================================================
     1.8  case eval_ist_monom 0 0 (str2term "12 ist_monom") 0 of
     1.9      SOME ("12 ist_monom = True", _) => ()
    1.10    | _ => error "polyminus.sml: 12 ist_monom = True";
    1.11 @@ -66,7 +65,6 @@
    1.12      SOME ("3 * a * b ist_monom = True", _) => ()
    1.13    | _ => error "polyminus.sml: 3*a*b ist_monom = True";
    1.14  
    1.15 -============ inhibit exn =====================================================*)
    1.16  
    1.17  "----------- watch order_add_mult  -------------------------------";
    1.18  "----------- watch order_add_mult  -------------------------------";
    1.19 @@ -303,13 +301,14 @@
    1.20  moveActiveRoot 1;
    1.21  autoCalculate 1 CompleteCalc;
    1.22  val ((pt,p),_) = get_calc 1; show_pt pt;
    1.23 -(*========== inhibit exn 110520 ================================================
    1.24 -"??.empty" came with getting preconditions into ctxt:
    1.25  
    1.26 +show_pt pt;
    1.27 +p;
    1.28 +(get_obj g_res pt (fst p));
    1.29 +term2str (get_obj g_res pt (fst p));
    1.30  if p = ([], Res) andalso 
    1.31     term2str (get_obj g_res pt (fst p)) = "3 + 3 * r + 6 * s - 8 * t"
    1.32  then () else error "polyminus.sml: Vereinfache 140 d)";
    1.33 -============ inhibit exn 110520 ==============================================*)
    1.34  
    1.35  
    1.36  "----------- 139 c ---";
    1.37 @@ -385,7 +384,6 @@
    1.38  @@@@@WN081114 gives "??.empty", all "Pruefe" are the same,
    1.39  although analogies work in interface.sml: FIXME.WN081114 in "Pruefe"*)
    1.40  val ((pt,p),_) = get_calc 1;
    1.41 -(*========== inhibit exn 110310 ================================================
    1.42  if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "11 = 11"
    1.43  then () else error "polyminus.sml: Probe 11 = 11";
    1.44  show_pt pt;
    1.45 @@ -665,4 +663,3 @@
    1.46      (2, [1], "#Find", Const (...), [...])]
    1.47     : ori list
    1.48  *)
    1.49 -============ inhibit exn 110310 ==============================================*)