1.1 --- a/test/Tools/isac/ProgLang/evaluate.sml	Tue May 19 12:33:35 2020 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml	Wed May 20 12:52:09 2020 +0200
     1.3 @@ -74,9 +74,9 @@
     1.4  "----------- calculate from Prog --------------------------------- -----------------------------";
     1.5  "----------- calculate from Prog --------------------------------- -----------------------------";
     1.6  val thy = @{theory "Test"};
     1.7 -val fmz = ["realTestGiven (((1+2)*4/3)^^^2)","realTestFind s"];
     1.8 +val fmz = ["realTestGiven (((1+2)*4/3)^^^2)", "realTestFind s"];
     1.9  val (dI',pI',mI') =
    1.10 -  ("Test",["calculate","test"],["Test","test_calculate"]);
    1.11 +  ("Test",["calculate", "test"],["Test", "test_calculate"]);
    1.12  
    1.13  val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    1.14  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.15 @@ -86,17 +86,17 @@
    1.16  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.17  (*nxt = ("Specify_Theory",Specify_Theory "Test") : string * tac*)
    1.18  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.19 -(*nxt = ("Specify_Problem",Specify_Problem ["calculate","test"])*)
    1.20 +(*nxt = ("Specify_Problem",Specify_Problem ["calculate", "test"])*)
    1.21  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.22 -(*nxt = ("Specify_Method",Specify_Method ("Test","test_calculate"))*)
    1.23 +(*nxt = ("Specify_Method",Specify_Method ("Test", "test_calculate"))*)
    1.24  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.25 -(*nxt = ("Apply_Method",Apply_Method ("Test","test_calculate"))*)
    1.26 +(*nxt = ("Apply_Method",Apply_Method ("Test", "test_calculate"))*)
    1.27  
    1.28  (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Calculate",Calculate "PLUS")*)
    1.29  (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Calculate",Calculate "TIMES")*)
    1.30  (*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Calculate",Calculate "DIVIDE")*)
    1.31  (*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Calculate",Calculate "POWER")*)
    1.32 -(*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Check_Postcond",Check_Postcond ["calculate","test"])*)
    1.33 +(*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Check_Postcond",Check_Postcond ["calculate", "test"])*)
    1.34  (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("End_Proof'",End_Proof')*)
    1.35  case f of Test_Out.FormKF "16" => () | _ =>
    1.36  error "evaluate.sml: script test_calculate changed behaviour";
    1.37 @@ -131,13 +131,13 @@
    1.38   val t = (Thm.term_of o the o (parse thy)) "6 / 2";
    1.39   val rls = Test_simplify;
    1.40   val (t,_) = the (rewrite_set_ thy false rls t);
    1.41 -(*val t = Free ("3","Real.real") : term*)
    1.42 +(*val t = Free ("3", "Real.real") : term*)
    1.43  
    1.44  (*--------------(3): is_const works ?: -------------------------------------*)
    1.45   val t = (Thm.term_of o the o (parse @{theory Test})) "2 is_const";
    1.46   atomty t;
    1.47   rewrite_set_ @{theory Test} false tval_rls t;
    1.48 -(*val it = SOME (Const ("HOL.True","bool"),[]) ... works*)
    1.49 +(*val it = SOME (Const ("HOL.True", "bool"),[]) ... works*)
    1.50  
    1.51   val t = str2term "2 * x is_const";
    1.52   val SOME (str,t') = eval_const "" "" t (@{theory "Isac_Knowledge"});