intermed: uncomment tests with CompleteCalc decompose-isar
authorThomas Leh <t.leh@gmx.at>
Tue, 19 Jul 2011 10:09:30 +0200
branchdecompose-isar
changeset 42111d0ba4fce4892
parent 42109 cd33f1f80c8a
child 42112 d9ee93f3e309
intermed: uncomment tests with CompleteCalc
test/Tools/isac/Knowledge/polyminus.sml
test/Tools/isac/Test_Some.thy
     1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml	Tue Jul 19 09:53:30 2011 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml	Tue Jul 19 10:09:30 2011 +0200
     1.3 @@ -550,6 +550,7 @@
     1.4  trace_rewrite := false;
     1.5  
     1.6  (*@@@@@@@*)
     1.7 +============ inhibit exn 110719 ==============================================*)
     1.8  states:=[];
     1.9  CalcTree [(["Term ((3*a + 2) * (4*a - 1))",
    1.10  	    "normalform N"],
    1.11 @@ -559,11 +560,13 @@
    1.12  autoCalculate 1 CompleteCalc;
    1.13  val ((pt,p),_) = get_calc 1; show_pt pt;
    1.14  
    1.15 -(*
    1.16 +
    1.17  if p = ([], Res) andalso 
    1.18 -   term2str (get_obj g_res pt (fst p)) = "1 + 14 * u"
    1.19 +   term2str (get_obj g_res pt (fst p)) = "-2 + 12 * a ^^^ 2 + 5 * a"
    1.20  then () else error "polyminus.sml: Vereinfache (2*u - 5 - (3 - ...";
    1.21 -*)
    1.22 +
    1.23 +(*=== inhibit exn ?=============================================================
    1.24 +
    1.25  ============ inhibit exn 110719 ==============================================*)
    1.26  
    1.27  
     2.1 --- a/test/Tools/isac/Test_Some.thy	Tue Jul 19 09:53:30 2011 +0200
     2.2 +++ b/test/Tools/isac/Test_Some.thy	Tue Jul 19 10:09:30 2011 +0200
     2.3 @@ -7,15 +7,20 @@
     2.4  
     2.5  ML{* writeln "**** run the test ***************************************" *}
     2.6  
     2.7 -use"../../../test/Tools/isac/Knowledge/polyminus.sml"  
     2.8 +use"../../../test/Tools/isac/Knowledge/polyminus.sml" 
     2.9  
    2.10  ML{*
    2.11 +
    2.12 +
    2.13  *}
    2.14  ML{*
    2.15 +
    2.16  *}
    2.17  ML{*
    2.18 +
    2.19  *}
    2.20  ML{*
    2.21 +
    2.22  *}
    2.23  ML{*
    2.24  *}