1.1 --- a/test/Tools/isac/Test_Isac.thy	Thu Mar 08 08:04:04 2018 +0100
     1.2 +++ b/test/Tools/isac/Test_Isac.thy	Thu Mar 08 12:30:46 2018 +0100
     1.3 @@ -294,8 +294,11 @@
     1.4    ML_file "Knowledge/integrate.sml"
     1.5  
     1.6  ML {*
     1.7 +"~~~~~ fun xxx, args:"; val () = ();
     1.8  *} ML {*
     1.9 -"----------- simplify by ruleset reducing make_ratpoly_in";
    1.10 +
    1.11 +*} ML {*
    1.12 +*} ML {*
    1.13  val thy = @{theory "Isac"};
    1.14  "===== test 1";
    1.15  val t = str2t "1/EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)";
    1.16 @@ -338,39 +341,32 @@
    1.17  @{thm separate_1_bdv_n}; (*::real ..because of ^^^*)
    1.18  (*show_types := false; --- do we need type-constraint in thms? YES ?!?!?!*)
    1.19  
    1.20 -val SOME (t, []) = rewrite_set_inst_ thy true subs rls t;
    1.21 +*} ML {*
    1.22 +"~~~~~ fun xxx, args:"; val () = ();
    1.23 +(*//==========================================================================================\\*)
    1.24 +*} ML {*
    1.25 +*} ML {*
    1.26 +*} ML {*
    1.27 +*} ML {*
    1.28 +*} ML {*
    1.29 +(*\\==========================================================================================//*)
    1.30 +"~~~~~ fun xxx, args:"; val () = ();
    1.31 +*} ML {*
    1.32 +(* isabisac <> isabisac15 *)
    1.33 +(*val SOME (t, []) = rewrite_set_inst_ thy true subs rls t;    isabisac15 *)
    1.34 +  val NONE = rewrite_set_inst_ thy true subs rls t;         (* isabisac   *)
    1.35 +*} text {*
    1.36  if term2str t = "1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2)" then ()
    1.37  else error "integrate.sml simplify by ruleset separate_bdv.. #4";
    1.38  
    1.39  "===== test 5";
    1.40 -val t = str2t "1/EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)";
    1.41 -val rls = simplify_Integral;
    1.42 -val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t;
    1.43 -(* given was:   "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)" *)
    1.44 -if term2str t = "1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2)" then ()
    1.45 -else error "integrate.sml, simplify_Integral #99";
    1.46 +*} ML {*
    1.47 +*}
    1.48  
    1.49 -"........... 2nd integral ........................................";
    1.50 -"........... 2nd integral ........................................";
    1.51 -"........... 2nd integral ........................................";
    1.52 -val t = str2t 
    1.53 -"Integral 1 / EI * (L * q_0 / 2 * (x ^^^ 2 / 2) + -1 * q_0 / 2 * (x ^^^ 3 / 3)) D x";
    1.54 -val rls = simplify_Integral;
    1.55 -val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t;
    1.56 -if term2str t =
    1.57 -   "Integral 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3) D x"
    1.58 -then () else raise error "integrate.sml, simplify_Integral #198";
    1.59  
    1.60 -val rls = integration_rules;
    1.61 -val SOME (t,[]) = rewrite_set_ thy true rls t;
    1.62 -term2str t;
    1.63 -if term2str t = 
    1.64 -   "1 / EI * (L * q_0 / 4 * (x ^^^ 3 / 3) + -1 * q_0 / 6 * (x ^^^ 4 / 4))"
    1.65 -then () else error "integrate.sml, simplify_Integral #199";
    1.66  
    1.67  
    1.68 -"----------- integrate by ruleset -----------------------";*} ML {*
    1.69 -*}
    1.70 +
    1.71  
    1.72    ML_file "Knowledge/eqsystem.sml"
    1.73    ML_file "Knowledge/test.sml"