1.1 --- a/test/Tools/isac/Knowledge/integrate.sml	Sun Oct 09 06:53:03 2022 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/integrate.sml	Sun Oct 09 07:44:22 2022 +0200
     1.3 @@ -51,14 +51,14 @@
     1.4  "----------- parsing ------------------------------------";
     1.5  "----------- parsing ------------------------------------";
     1.6  "----------- parsing ------------------------------------";
     1.7 -val t = TermC.str2term "Integral x D x";
     1.8 -val t = TermC.str2term "Integral x \<up> 2 D x";
     1.9 +val t = TermC.parse_test @{context} "Integral x D x";
    1.10 +val t = TermC.parse_test @{context} "Integral x \<up> 2 D x";
    1.11  case t of 
    1.12      Const (\<^const_name>\<open>Integral\<close>, _) $
    1.13       (Const (\<^const_name>\<open>realpow\<close>, _) $ Free _ $ _) $ Free ("x", _) => ()
    1.14    | _ => error "integrate.sml: parsing: Integral x \<up> 2 D x";
    1.15  
    1.16 -val t = TermC.str2term "ff x is_f_x";
    1.17 +val t = TermC.parse_test @{context} "ff x is_f_x";
    1.18  case t of Const (\<^const_name>\<open>is_f_x\<close>, _) $ _ => ()
    1.19  	| _ => error "integrate.sml: parsing: ff x is_f_x";
    1.20  
    1.21 @@ -66,26 +66,26 @@
    1.22  "----------- integrate by rewriting ---------------------";
    1.23  "----------- integrate by rewriting ---------------------";
    1.24  "----------- integrate by rewriting ---------------------";
    1.25 -val str = rewrit @{thm "integral_const"} (TermC.str2term "Integral 1 D x");
    1.26 +val str = rewrit @{thm "integral_const"} (TermC.parse_test @{context} "Integral 1 D x");
    1.27  if term2s str = "1 * x" then () else error "integrate.sml Integral 1 D x";
    1.28  
    1.29 -val str = rewrit @{thm "integral_const"} (TermC.str2term  "Integral M'/EJ D x");
    1.30 +val str = rewrit @{thm "integral_const"} (TermC.parse_test @{context}  "Integral M'/EJ D x");
    1.31  if term2s str = "M' / EJ * x" then ()
    1.32  else error "Integral M'/EJ D x   BY integral_const";
    1.33  
    1.34 -val str = rewrit @{thm "integral_var"} (TermC.str2term "Integral x D x");
    1.35 +val str = rewrit @{thm "integral_var"} (TermC.parse_test @{context} "Integral x D x");
    1.36  if term2s str = "x \<up> 2 / 2" then ()
    1.37  else error "Integral x D x   BY integral_var";
    1.38  
    1.39 -val str = rewrit @{thm "integral_add"} (TermC.str2term "Integral x + 1 D x");
    1.40 +val str = rewrit @{thm "integral_add"} (TermC.parse_test @{context} "Integral x + 1 D x");
    1.41  if term2s str = "Integral x D x + Integral 1 D x" then ()
    1.42  else error "Integral x + 1 D x   BY integral_add";
    1.43  
    1.44 -val str = rewrit @{thm "integral_mult"} (TermC.str2term "Integral M'/EJ * x \<up> 3 D x");
    1.45 +val str = rewrit @{thm "integral_mult"} (TermC.parse_test @{context} "Integral M'/EJ * x \<up> 3 D x");
    1.46  if term2s str = "M' / EJ * Integral x \<up> 3 D x" then ()
    1.47  else error "Integral M'/EJ * x \<up> 3 D x   BY integral_mult";
    1.48  
    1.49 -val str = rewrit @{thm "integral_pow"} (TermC.str2term "Integral x \<up> 3 D x");
    1.50 +val str = rewrit @{thm "integral_pow"} (TermC.parse_test @{context} "Integral x \<up> 3 D x");
    1.51  if term2s str = "x \<up> (3 + 1) / (3 + 1)" then ()
    1.52  else error "integrate.sml Integral x \<up> 3 D x";
    1.53  
    1.54 @@ -93,7 +93,7 @@
    1.55  "----------- test add_new_c, TermC.is_f_x ---------------------";
    1.56  "----------- test add_new_c, TermC.is_f_x ---------------------";
    1.57  "----------- test add_new_c, TermC.is_f_x ---------------------";
    1.58 -val term = TermC.str2term "x \<up> 2 * c + c_2";
    1.59 +val term = TermC.parse_test @{context} "x \<up> 2 * c + c_2";
    1.60  val cc = new_c term;
    1.61  if UnparseC.term cc = "c_3" then () else error "integrate.sml: new_c ???";
    1.62  
    1.63 @@ -108,7 +108,7 @@
    1.64  if UnparseC.term t' = "x \<up> 2 * c + c_2 + c_3" then ()
    1.65  else error "intergrate.sml: diff. rewrite_set add_new_c 1";
    1.66  
    1.67 -val term = TermC.str2term "ff x = x \<up> 2*c + c_2";
    1.68 +val term = TermC.parse_test @{context} "ff x = x \<up> 2*c + c_2";
    1.69  val SOME (t',_) = rewrite_set_ ctxt true add_new_c term;
    1.70  if UnparseC.term t' = "ff x = x \<up> 2 * c + c_2 + c_3" then ()
    1.71  else error "intergrate.sml: diff. rewrite_set add_new_c 2";
    1.72 @@ -173,9 +173,9 @@
    1.73  "----------- simplify by ruleset reducing make_ratpoly_in";
    1.74  val thy = @{theory "Isac_Knowledge"};
    1.75  val ctxt = Proof_Context.init_global thy;
    1.76 -val subst = [(TermC.str2term "bdv ::real", TermC.str2term "x ::real")]; (*DOESN'T HELP*)
    1.77 +val subst = [(TermC.parse_test @{context} "bdv ::real", TermC.parse_test @{context} "x ::real")]; (*DOESN'T HELP*)
    1.78  "===== test 1";
    1.79 -val t = TermC.str2term "1/EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)";
    1.80 +val t = TermC.parse_test @{context} "1/EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)";
    1.81  
    1.82  "----- stepwise from the rulesets in simplify_Integral and below-----";
    1.83  val rls = norm_Rational_noadd_fractions;
    1.84 @@ -196,7 +196,7 @@
    1.85  else error "integrate.sml simplify by ruleset discard_parenth.. #3";
    1.86  
    1.87  "===== test 4";
    1.88 -val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")];
    1.89 +val subs = [(TermC.parse_test @{context} "bdv::real", TermC.parse_test @{context} "x::real")];
    1.90  val rls = 
    1.91    (Rule_Set.append_rules "separate_bdv" collect_bdv
    1.92   	  [Thm ("separate_bdv", @{thm separate_bdv}),
    1.93 @@ -221,7 +221,7 @@
    1.94  else error "integrate.sml simplify by ruleset separate_bdv.. #4";
    1.95  
    1.96  "===== test 5";
    1.97 -val t = TermC.str2term "1/EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)";
    1.98 +val t = TermC.parse_test @{context} "1/EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)";
    1.99  val rls = simplify_Integral;
   1.100  val SOME (t,[]) = rewrite_set_inst_ ctxt true subs rls t;
   1.101  (* given was:   "1 / EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)" *)
   1.102 @@ -231,10 +231,10 @@
   1.103  "........... 2nd integral ........................................";
   1.104  "........... 2nd integral ........................................";
   1.105  "........... 2nd integral ........................................";
   1.106 -val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")];
   1.107 +val subs = [(TermC.parse_test @{context} "bdv::real", TermC.parse_test @{context} "x::real")];
   1.108  
   1.109  val thy = @{theory Biegelinie};
   1.110 -val t = TermC.str2term 
   1.111 +val t = TermC.parse_test @{context} 
   1.112    "Integral 1 / EI * (L * q_0 / 2 * (x \<up> 2 / 2) + - 1 * q_0 / 2 * (x \<up> 3 / 3)) D x";
   1.113  
   1.114  val rls = simplify_Integral;
   1.115 @@ -309,7 +309,7 @@
   1.116  "----------- rewrite 3rd integration in 7.27 ------------";
   1.117  "----------- rewrite 3rd integration in 7.27 ------------";
   1.118  "----------- rewrite 3rd integration in 7.27 ------------";
   1.119 -val t = TermC.str2term "Integral 1 / EI * ((L * q_0 * x + - 1 * q_0 * x \<up> 2) / 2) D x";
   1.120 +val t = TermC.parse_test @{context} "Integral 1 / EI * ((L * q_0 * x + - 1 * q_0 * x \<up> 2) / 2) D x";
   1.121  val SOME(t, _)= rewrite_set_inst_ ctxt true subs simplify_Integral t;
   1.122  if UnparseC.term t = 
   1.123    "Integral 1 / EI * (L * q_0 / 2 * x + - 1 * q_0 / 2 * x \<up> 2) D x"
   1.124 @@ -358,7 +358,7 @@
   1.125  if F1_ = F2_ then () else error "integrate.sml: unequal find's";
   1.126  
   1.127  val ((dsc as Const (\<^const_name>\<open>antiDerivativeName\<close>, _)) 
   1.128 -	 $ Free ("ff", F3_type)) = TermC.str2term "antiDerivativeName ff";
   1.129 +	 $ Free ("ff", F3_type)) = TermC.parse_test @{context} "antiDerivativeName ff";
   1.130  if Input_Descript.is_a dsc then () else error "integrate.sml: no description";
   1.131  if F1_type = F3_type then () 
   1.132  else error "integrate.sml: unequal types in find's";