test/Tools/isac/Knowledge/diophanteq.sml
changeset 60329 0c10aeff57d7
parent 59997 46fe5a8c3911
child 60337 cbad4e18e91b
     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;