1.1 --- a/test/Tools/isac/Knowledge/biegelinie-1.sml	Sun Oct 09 06:53:03 2022 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/biegelinie-1.sml	Sun Oct 09 07:44:22 2022 +0200
     1.3 @@ -29,23 +29,22 @@
     1.4  
     1.5  val thy = @{theory "Biegelinie"};
     1.6  val ctxt = ThyC.id_to_ctxt "Biegelinie";
     1.7 -fun str2term str = TermC.parseNEW' ctxt str;
     1.8  fun term2s t = UnparseC.term_by_thyID "Biegelinie" t;
     1.9  fun rewrit thm str = fst (the (rewrite_ ctxt tless_true Rule_Set.empty true thm str));
    1.10  
    1.11  "----------- the rules -------------------------------------------";
    1.12  "----------- the rules -------------------------------------------";
    1.13  "----------- the rules -------------------------------------------";
    1.14 -val t = rewrit @{thm Belastung_Querkraft} (TermC.str2term "- qq x = - q_0"); term2s t;
    1.15 +val t = rewrit @{thm Belastung_Querkraft} (TermC.parse_test @{context} "- qq x = - q_0"); term2s t;
    1.16  if term2s t = "Q' x = - q_0" then ()
    1.17  else error  "/biegelinie.sml: Belastung_Querkraft";
    1.18  
    1.19 -val t = rewrit @{thm Querkraft_Moment} (TermC.str2term "Q x = - q_0 * x + c"); term2s t;
    1.20 +val t = rewrit @{thm Querkraft_Moment} (TermC.parse_test @{context} "Q x = - q_0 * x + c"); term2s t;
    1.21  if term2s t = "?M_b' x = - q_0 * x + c" then ()
    1.22  (*if term2s t = "M_b' x = - q_0 * x + c" then ()  cf.fbe1652b0df8 new handling of quotes in mixfix*)
    1.23  else error  "/biegelinie.sml: Querkraft_Moment";
    1.24  
    1.25 -val t = rewrit @{thm Moment_Neigung} (TermC.str2term "M_b x = -q_0 * x \<up> 2/2 + q_0/2 *L*x");
    1.26 +val t = rewrit @{thm Moment_Neigung} (TermC.parse_test @{context} "M_b x = -q_0 * x \<up> 2/2 + q_0/2 *L*x");
    1.27      term2s t;
    1.28  if term2s t = "- EI * y'' x = - q_0 * x \<up> 2 / 2 + q_0 / 2 * L * x" then ()
    1.29  else error  "biegelinie.sml: Moment_Neigung";
    1.30 @@ -71,13 +70,13 @@
    1.31  			 Eval("Prog_Expr.argument_in", eval_argument_in "Prog_Expr.argument_in")
    1.32  			 ],
    1.33  		scr = Empty_Prog};
    1.34 -val rm_ = TermC.str2term"[M_b 0 = 0, M_b L = 0]";
    1.35 -val M__ = TermC.str2term"M_b x = - 1 * x \<up> 2 / 2 + x * c + c_2";
    1.36 +val rm_ = TermC.parse_test @{context}"[M_b 0 = 0, M_b L = 0]";
    1.37 +val M__ = TermC.parse_test @{context}"M_b x = - 1 * x \<up> 2 / 2 + x * c + c_2";
    1.38  val SOME (e1__,_) = rewrite_set_ ctxt false srls 
    1.39 -  (TermC.str2term "(NTH::[real,bool list]=>bool) 1 " $ rm_);
    1.40 +  (TermC.parse_test @{context} "(NTH::[real,bool list]=>bool) 1 " $ rm_);
    1.41  if UnparseC.term e1__ = "M_b 0 = 0" then () else error "biegelinie.sml simplify NTH 1 rm_";
    1.42  
    1.43 -val SOME (x1__,_) = rewrite_set_ ctxt false srls (TermC.str2term "argument_in (lhs (M_b 0 = 0))");
    1.44 +val SOME (x1__,_) = rewrite_set_ ctxt false srls (TermC.parse_test @{context} "argument_in (lhs (M_b 0 = 0))");
    1.45  if UnparseC.term x1__ = "0" then ()
    1.46  else error "biegelinie.sml simplify argument_in (lhs (M_b 0 = 0)";
    1.47  
    1.48 @@ -115,8 +114,8 @@
    1.49  "----------- investigate normalforms in biegelinien --------------";
    1.50  "----------- investigate normalforms in biegelinien --------------";
    1.51  "----- coming from integration, kept for later improvements:";
    1.52 -val Q = TermC.str2term "Q x = c + - 1 * q_0 * x";
    1.53 -val M_b = TermC.str2term "M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2";
    1.54 -val y' = TermC.str2term "y' x = c_3 + 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3)";
    1.55 -val y = TermC.str2term "y x = c_4 + c_3 * x +\n1 / (- 1 * EI) * (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)";
    1.56 +val Q = TermC.parse_test @{context} "Q x = c + - 1 * q_0 * x";
    1.57 +val M_b = TermC.parse_test @{context} "M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2";
    1.58 +val y' = TermC.parse_test @{context} "y' x = c_3 + 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3)";
    1.59 +val y = TermC.parse_test @{context} "y x = c_4 + c_3 * x +\n1 / (- 1 * EI) * (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)";
    1.60  (* \<up>   1 / (- 1 * EI) NOT distributed - ok! \<up> \<up> \<up> \<up> \<up> \<up>  \<up> ^^*)