1.1 --- a/test/Tools/isac/Knowledge/eqsystem-2.sml	Thu Jul 28 11:43:27 2022 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/eqsystem-2.sml	Sat Jul 30 16:47:45 2022 +0200
     1.3 @@ -3,7 +3,6 @@
     1.4     (c) due to copyright terms
     1.5  *)
     1.6  
     1.7 -Rewrite.trace_on := false; (*true false*)
     1.8  "-----------------------------------------------------------------";
     1.9  "table of contents -----------------------------------------------";
    1.10  "-----------------------------------------------------------------";
    1.11 @@ -130,26 +129,26 @@
    1.12    "0 = c_4 + L * c_3 +(12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 24 * EI), " ^
    1.13    "0 = c_2, " ^
    1.14    "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]");
    1.15 -val SOME (t, _) = rewrite_set_ thy false isolate_bdvs_4x4 t;
    1.16 +val SOME (t, _) = rewrite_set_ ctxt false isolate_bdvs_4x4 t;
    1.17  if UnparseC.term t =
    1.18  "[c_4 = 0,\n (12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) /\n (- 24 * EI) =\n - 1 * (c_4 + L * c_3) + 0,\n c_2 = 0, (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2 = 0]"
    1.19  then () else error "Bsp 7.27";
    1.20  
    1.21  "----- Bsp 7.27 go through the rewrites in met_eqsys_norm_4x4";
    1.22  val t = TermC.str2term "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2";
    1.23 -val NONE = rewrite_set_ thy false norm_Rational t;
    1.24 +val NONE = rewrite_set_ ctxt false norm_Rational t;
    1.25  val SOME (t,_) = 
    1.26 -    rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
    1.27 +    rewrite_set_inst_ ctxt false subst simplify_System_parenthesized t;
    1.28  if UnparseC.term t = "0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)"
    1.29  then () else error "Bsp 7.27 go through the rewrites in met_eqsys_norm_4x4";
    1.30  
    1.31  "--- isolate_bdvs_4x4";
    1.32  (*
    1.33 -val SOME (t,_) = rewrite_set_inst_ thy false subst isolate_bdvs_4x4 t;
    1.34 +val SOME (t,_) = rewrite_set_inst_ ctxt false subst isolate_bdvs_4x4 t;
    1.35  UnparseC.term t;
    1.36 -val SOME (t,_) = rewrite_set_inst_ thy false subst simplify_System t;
    1.37 +val SOME (t,_) = rewrite_set_inst_ ctxt false subst simplify_System t;
    1.38  UnparseC.term t;
    1.39 -val SOME (t,_) = rewrite_set_ thy false order_system t;
    1.40 +val SOME (t,_) = rewrite_set_ ctxt false order_system t;
    1.41  UnparseC.term t;
    1.42  *)
    1.43  
    1.44 @@ -208,29 +207,29 @@
    1.45    "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, " ^
    1.46    "0 = c_4, " ^
    1.47    "0 = c_3]");
    1.48 -val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t;
    1.49 -val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t;
    1.50 -val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t;
    1.51 +val SOME (t,_) = rewrite_ ctxt e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t;
    1.52 +val SOME (t,_) = rewrite_ ctxt e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t;
    1.53 +val SOME (t,_) = rewrite_ ctxt e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t;
    1.54  if UnparseC.term t = 
    1.55    "[L * q_0 = c, (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2 = 0,\n c_4 = 0, c_3 = 0]"
    1.56  then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 1";
    1.57  
    1.58 -val SOME (t,_) = rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
    1.59 +val SOME (t,_) = rewrite_set_inst_ ctxt false subst simplify_System_parenthesized t;
    1.60  if UnparseC.term t = "[L * q_0 = c, - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2) = 0, c_4 = 0,\n c_3 = 0]"
    1.61  then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 2";
    1.62  
    1.63 -val SOME (t,_) = rewrite_set_inst_ thy false subst isolate_bdvs_4x4 t;
    1.64 +val SOME (t,_) = rewrite_set_inst_ ctxt false subst isolate_bdvs_4x4 t;
    1.65  if UnparseC.term t =
    1.66     "[c = (- 1 * (L * q_0) + 0) / - 1,\n" ^ 
    1.67     " L * c + c_2 = - 1 * (- 1 * q_0 * L \<up> 2 / 2) + 0, c_4 = 0, c_3 = 0]"
    1.68  then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 3";
    1.69  
    1.70 -val SOME (t,_) = rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
    1.71 +val SOME (t,_) = rewrite_set_inst_ ctxt false subst simplify_System_parenthesized t;
    1.72  if UnparseC.term t =
    1.73    "[c = - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_4 = 0,\n c_3 = 0]"
    1.74  then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 4";
    1.75  
    1.76 -val SOME (t, _) = rewrite_set_ thy false order_system t;
    1.77 +val SOME (t, _) = rewrite_set_ ctxt false order_system t;
    1.78  if UnparseC.term t =
    1.79    "[c = - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_3 = 0,\n c_4 = 0]"
    1.80  then () else error "eqsystem.sml: exp 7.70 normalise 4x4 by rewrite changed";