1.1 --- a/test/Tools/isac/Knowledge/diophanteq.sml Fri Jul 16 07:45:06 2021 +0200
1.2 +++ b/test/Tools/isac/Knowledge/diophanteq.sml Sat Jul 17 14:05:28 2021 +0200
1.3 @@ -67,7 +67,7 @@
1.4 val thy = @{theory "Test"};
1.5 "----------- rewriting for usecase2 ---------------------";
1.6
1.7 -val t = case parseNEW ctxt "xxx + abc + -1 * 111 + (123::int)" of
1.8 +val t = case parseNEW ctxt "xxx + abc + - 1 * 111 + (123::int)" of
1.9 SOME t' => t'
1.10 | NONE => error "diophanteq.sml: syntax error in rewriting for usecase2";
1.11
1.12 @@ -83,12 +83,12 @@
1.13 "----------- mathengine with usecase2 -------------------";
1.14 val p = e_pos'; val c = [];
1.15 val (fmz, (thy, pbl, met)) =
1.16 - (["intTestGiven (xxx + abc + -1 * 111 + (123::int))", "intTestFind sss"],
1.17 + (["intTestGiven (xxx + abc + - 1 * 111 + (123::int))", "intTestFind sss"],
1.18 (Context.theory_name thy, ["inttype", "test"], ["Test", "intsimp"]));
1.19 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (thy, pbl, met))];
1.20 (*nxt = ("Model_Problem", ...)*)
1.21 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.22 -(*nxt = ("Add_Given", Add_Given "intTestGiven (xxx + abc + -1 * 111 + 123)")*)
1.23 +(*nxt = ("Add_Given", Add_Given "intTestGiven (xxx + abc + - 1 * 111 + 123)")*)
1.24 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.25 (* Add_Find ###########################################*)
1.26 val (p,_,f,nxt,_,pt) = me nxt p c pt;