1.1 --- a/test/Tools/isac/Knowledge/eqsystem-2.sml	Sun Sep 12 15:40:15 2021 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/eqsystem-2.sml	Sun Sep 12 15:53:36 2021 +0200
     1.3 @@ -226,15 +226,13 @@
     1.4  then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 3";
     1.5  
     1.6  val SOME (t,_) = rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
     1.7 -if UnparseC.term t =(*BEFORE "eliminate ThmC.numerals_to_Free"..
     1.8 -  "[c = - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_4 = 0, c_3 = 0]"*)
     1.9 -  "[c = - 0 + - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_4 = 0,\n c_3 = 0]"
    1.10 +if UnparseC.term t =
    1.11 +  "[c = - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_4 = 0,\n c_3 = 0]"
    1.12  then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 4";
    1.13  
    1.14  val SOME (t, _) = rewrite_set_ thy false order_system t;
    1.15 -if UnparseC.term t =(*BEFORE "eliminate ThmC.numerals_to_Free"..
    1.16 -  "[c = - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_3 = 0, c_4 = 0]"*)
    1.17 -  "[c = - 0 + - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_3 = 0,\n c_4 = 0]"
    1.18 +if UnparseC.term t =
    1.19 +  "[c = - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_3 = 0,\n c_4 = 0]"
    1.20  then () else error "eqsystem.sml: exp 7.70 normalise 4x4 by rewrite changed";
    1.21  
    1.22  "----- 7.70 with met normalise: ";

     2.1 --- a/test/Tools/isac/Test_Isac_Short.thy	Sun Sep 12 15:40:15 2021 +0200
     2.2 +++ b/test/Tools/isac/Test_Isac_Short.thy	Sun Sep 12 15:53:36 2021 +0200
     2.3 @@ -302,7 +302,7 @@
     2.4    ML_file "Knowledge/diff.sml"
     2.5    ML_file "Knowledge/integrate.sml"
     2.6    ML_file "Knowledge/eqsystem-1.sml"
     2.7 -(*ML_file "Knowledge/eqsystem-2.sml"   broken by TOODOO 8e46f61fdb15 *)
     2.8 +  ML_file "Knowledge/eqsystem-2.sml"
     2.9    ML_file "Knowledge/test.sml"
    2.10    ML_file "Knowledge/polyminus.sml"
    2.11    ML_file "Knowledge/vect.sml"