test/Tools/isac/Knowledge/diophanteq.sml
branchdecompose-isar
changeset 41934 95407f7fe14a
parent 41933 8d38adf87848
child 41936 c12d6f2a11aa
     1.1 --- a/test/Tools/isac/Knowledge/diophanteq.sml	Fri Mar 18 09:26:03 2011 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/diophanteq.sml	Fri Mar 18 12:33:12 2011 +0100
     1.3 @@ -4,6 +4,7 @@
     1.4  12345678901234567890123456789012345678901234567890123456789012345678901234567890
     1.5          10        20        30        40        50        60        70        80
     1.6  *)
     1.7 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
     1.8  "--------------------------------------------------------";
     1.9  "table of contents --------------------------------------";
    1.10  "--------------------------------------------------------";
    1.11 @@ -39,15 +40,15 @@
    1.12  "----------- mathengine with usecase1 -------------------";
    1.13  "----------- mathengine with usecase1 -------------------";
    1.14  "----------- mathengine with usecase1 -------------------";
    1.15 -val p = e_pos'; val c = []; 
    1.16 -val (p,_,f,nxt,_,pt) = 
    1.17 -    CalcTreeTEST 
    1.18 -        [(["boolTestGiven (xxx + 111 = abc + (123::int))", "intTestGiven (xxx::int)", "boolTestFind sss"],
    1.19 -          (Context.theory_name thy, 
    1.20 -  ["diophantine","equation"], ["Test","solve_diophant"]))];
    1.21 -"----- step 1: returns nxt = Add_Given \"functionTerm (x ^^^ 2 + 1)\" ---";
    1.22 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
    1.23 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
    1.24 +val p = e_pos'; val c = [];
    1.25 +val (fmz, (thy, pbl, met)) = 
    1.26 +  (["intTestGiven (xxx + abc + -1 * 111 + (123::int))", "intTestFind sss"],
    1.27 +   (Context.theory_name thy, ["diophantine", "equation"], 
    1.28 +    ["Test", "solve_diophant"]));
    1.29 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (thy, pbl, met))];
    1.30  val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    1.31 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
    1.32  val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    1.33  val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    1.34  val (p,_,f,nxt,_,pt) = me nxt p c pt;