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;