1.1 --- a/test/Tools/isac/Test_Isac_Short.thy	Thu Jul 15 14:10:18 2021 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac_Short.thy	Thu Jul 15 20:02:16 2021 +0200
     1.3 @@ -512,13 +512,14 @@
     1.4  \<close> ML \<open>
     1.5  (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "ordne_alphabetisch"*)
     1.6  \<close> ML \<open>
     1.7 -val Test_Out.FormKF "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12" = f
     1.8 +(*+*)val Test_Out.FormKF "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12" = f
     1.9  \<close> ML \<open>
    1.10  (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "fasse_zusammen"*)
    1.11  
    1.12  \<close> ML \<open>
    1.13 -f
    1.14 +(*+*)val Test_Out.FormKF "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g" = f
    1.15  \<close> ML \<open>
    1.16 +\<close> ML \<open> (*GOON*)
    1.17  map Tactic.input_to_string (specific_from_prog pt p)
    1.18  \<close> ML \<open>
    1.19  (*+*)if map Tactic.input_to_string (specific_from_prog pt p) =
    1.20 @@ -971,6 +972,18 @@
    1.21    ML_file "Knowledge/descript.sml"
    1.22    ML_file "Knowledge/simplify.sml"
    1.23    ML_file "Knowledge/poly.sml"
    1.24 +ML \<open>
    1.25 +\<close> ML \<open>
    1.26 +\<close> ML \<open>
    1.27 +\<close> ML \<open>
    1.28 +\<close> ML \<open>
    1.29 +\<close> ML \<open>
    1.30 +\<close> ML \<open>
    1.31 +\<close> ML \<open>
    1.32 +\<close> ML \<open>
    1.33 +\<close> ML \<open>
    1.34 +\<close> ML \<open>
    1.35 +\<close>
    1.36    ML_file "Knowledge/gcd_poly_ml.sml"
    1.37    ML_file "Knowledge/gcd_poly_winkler.sml" (*must be after gcd_poly_ml.sml: redefines functions*)
    1.38    ML_file "Knowledge/rational.sml"                                            (*Test_Isac_Short*)