test/Tools/isac/Knowledge/eqsystem-2.sml
changeset 60565 f92963a33fe3
parent 60556 486223010ea8
child 60567 bb3140a02f3d
     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)]";