1.1 --- a/test/Tools/isac/Knowledge/eqsystem-2.sml Sun Oct 09 06:53:03 2022 +0200
1.2 +++ b/test/Tools/isac/Knowledge/eqsystem-2.sml Sun Oct 09 07:44:22 2022 +0200
1.3 @@ -108,8 +108,8 @@
1.4 "----------- all systems from Biegelinie -------------------------";
1.5 val thy = @{theory Isac_Knowledge}
1.6 val subst =
1.7 - [(TermC.str2term "bdv_1", TermC.str2term "c"), (TermC.str2term "bdv_2", TermC.str2term "c_2"),
1.8 - (TermC.str2term "bdv_3", TermC.str2term "c_3"), (TermC.str2term "bdv_4", TermC.str2term "c_4")];
1.9 + [(TermC.parse_test @{context} "bdv_1", TermC.parse_test @{context} "c"), (TermC.parse_test @{context} "bdv_2", TermC.parse_test @{context} "c_2"),
1.10 + (TermC.parse_test @{context} "bdv_3", TermC.parse_test @{context} "c_3"), (TermC.parse_test @{context} "bdv_4", TermC.parse_test @{context} "c_4")];
1.11
1.12 "------- Bsp 7.27";
1.13 States.reset ();
1.14 @@ -125,7 +125,7 @@
1.15 c c_2 c_3 c_4 c c_2 1->2: c
1.16 c_2 c_4
1.17 c c_2 c c_2 c_3 c_4 [2':c, 1:c_2, 3:c_4] -> 4:c_3*)
1.18 -val t = TermC.str2term
1.19 +val t = TermC.parse_test @{context}
1.20 ("[0 = c_4, " ^
1.21 "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.22 "0 = c_2, " ^
1.23 @@ -136,7 +136,7 @@
1.24 then () else error "Bsp 7.27";
1.25
1.26 "----- Bsp 7.27 go through the rewrites in met_eqsys_norm_4x4";
1.27 -val t = TermC.str2term "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2";
1.28 +val t = TermC.parse_test @{context} "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2";
1.29 val NONE = rewrite_set_ ctxt false norm_Rational t;
1.30 val SOME (t,_) =
1.31 rewrite_set_inst_ ctxt false subst simplify_System_parenthesized t;
1.32 @@ -181,7 +181,7 @@
1.33 c c_2 c_3 c_4 c c_2 c_3 1:c_3 -> 2:c c_2 2: c c_2
1.34 c_3 c_4
1.35 c c_2 c_3 c c_2 c_3 c_4 3:c_4 -> 4:c c_2 c_3 1:c_3 -> 4:c c_2*)
1.36 -val t = TermC.str2term
1.37 +val t = TermC.parse_test @{context}
1.38 ("[0 = c_4 + 0 / (- 1 * EI), " ^
1.39 "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.40 "0 = c_3 + 0 / (- 1 * EI), " ^
1.41 @@ -203,7 +203,7 @@
1.42 c_4 | STOPPED.WN06? test methods @@@@@@@@@@@@@@@@@@@@@@@*)
1.43
1.44 "----- 7.70 go through the rewrites in met_eqsys_norm_4x4";
1.45 -val t = TermC.str2term
1.46 +val t = TermC.parse_test @{context}
1.47 ("[L * q_0 = c, " ^
1.48 "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, " ^
1.49 "0 = c_4, " ^
1.50 @@ -321,7 +321,7 @@
1.51 c_4 | c_3 |2:c_3 -> 4' :c c_2 c_4 | |
1.52 c c_2 c_3 c_4 | c_4 |3' | |
1.53 c_3 |c c_2 c_3 c_4 |3:c_4 -> 4'':c c_2 |4'':c c_2 | *)
1.54 -val t = TermC.str2term"[0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, \
1.55 +val t = TermC.parse_test @{context}"[0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, \
1.56 \ 0 = c_4 + 0 / (- 1 * EI), \
1.57 \ 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.58 \ 0 = c_3 + 0 / (- 1 * EI)]";
1.59 @@ -356,7 +356,7 @@
1.60 c c_2 | |1:c_2 -> 2':c |c_2 c
1.61 c_4 | | |
1.62 c c_2 c_3 c_4 | |3:c_4 -> 4':c c_2 c_3 |c_2 c c_3*)
1.63 -val t = TermC.str2term"[0 = c_2, \
1.64 +val t = TermC.parse_test @{context}"[0 = c_2, \
1.65 \ 0 = (6 * c_2 + 6 * L * c + - 1 * L \<up> 2 * q_0) / 6, \
1.66 \ 0 = c_4 + 0 / (- 1 * EI), \
1.67 \ 0 = c_4 + L * c_3 + (60 * L \<up> 2 * c_2 + 20 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 120 * EI)]";