1.1 --- a/src/Tools/isac/Knowledge/Test.thy Thu Sep 23 08:43:36 2010 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Test.thy Thu Sep 23 08:54:26 2010 +0200
1.3 @@ -522,7 +522,7 @@
1.4 (["equation","test"],
1.5 [("#Given" ,["equality e_e","solveFor v_v"]),
1.6 ("#Where" ,["matches (?a = ?b) e_e"]),
1.7 - ("#Find" ,["solutions v'i'"])
1.8 + ("#Find" ,["solutions v_v'i'"])
1.9 ],
1.10 assoc_rls "matches",
1.11 SOME "solve (e_e::bool, v_v)", []));
1.12 @@ -543,7 +543,7 @@
1.13 [("#Given" ,["equality e_e","solveFor v_v"]),
1.14 ("#Where" ,["(matches ( v_v = 0) e_e) | (matches ( ?b*v_v = 0) e_e) |" ^
1.15 "(matches (?a+v_v = 0) e_e) | (matches (?a+?b*v_v = 0) e_e) "]),
1.16 - ("#Find" ,["solutions v'i'"])
1.17 + ("#Find" ,["solutions v_v'i'"])
1.18 ],
1.19 assoc_rls "matches",
1.20 SOME "solve (e_e::bool, v_v)", [["Test","solve_linear"]]));
1.21 @@ -595,7 +595,7 @@
1.22 (["Test","solve_linear"]:metID,
1.23 [("#Given" ,["equality e_e","solveFor v_v"]),
1.24 ("#Where" ,["matches (?a = ?b) e_e"]),
1.25 - ("#Find" ,["solutions v'i'"])
1.26 + ("#Find" ,["solutions v_v'i'"])
1.27 ],
1.28 {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls,
1.29 prls = assoc_rls "matches", calc = [], crls = tval_rls,
1.30 @@ -783,7 +783,7 @@
1.31 "(matches ( ?b*v_v ^^^2 = 0) e_e) |" ^
1.32 "(matches (?a + v_v ^^^2 = 0) e_e) |" ^
1.33 "(matches ( v_v ^^^2 = 0) e_e)"]),
1.34 - ("#Find" ,["solutions v'i'"])
1.35 + ("#Find" ,["solutions v_v'i'"])
1.36 ],
1.37 assoc_rls "matches",
1.38 SOME "solve (e_e::bool, v_v)", [["Test","solve_plain_square"]]));
1.39 @@ -817,7 +817,7 @@
1.40 (["polynomial","univariate","equation","test"],
1.41 [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
1.42 ("#Where" ,["False"]),
1.43 - ("#Find" ,["solutions v'i'"])
1.44 + ("#Find" ,["solutions v_v'i'"])
1.45 ],
1.46 e_rls, SOME "solve (e_e::bool, v_v)", []));
1.47
1.48 @@ -825,7 +825,7 @@
1.49 (prep_pbt thy "pbl_test_uni_poly_deg2" [] e_pblID
1.50 (["degree_two","polynomial","univariate","equation","test"],
1.51 [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
1.52 - ("#Find" ,["solutions v'i'"])
1.53 + ("#Find" ,["solutions v_v'i'"])
1.54 ],
1.55 e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", []));
1.56
1.57 @@ -833,7 +833,7 @@
1.58 (prep_pbt thy "pbl_test_uni_poly_deg2_pq" [] e_pblID
1.59 (["pq_formula","degree_two","polynomial","univariate","equation","test"],
1.60 [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
1.61 - ("#Find" ,["solutions v'i'"])
1.62 + ("#Find" ,["solutions v_v'i'"])
1.63 ],
1.64 e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", []));
1.65
1.66 @@ -841,7 +841,7 @@
1.67 (prep_pbt thy "pbl_test_uni_poly_deg2_abc" [] e_pblID
1.68 (["abc_formula","degree_two","polynomial","univariate","equation","test"],
1.69 [("#Given" ,["equality (a_a * x ^^^2 + b_b * x + c_c = 0)","solveFor v_v"]),
1.70 - ("#Find" ,["solutions v'i'"])
1.71 + ("#Find" ,["solutions v_v'i'"])
1.72 ],
1.73 e_rls, SOME "solve (a_a * x ^^^2 + b_b * x + c_c = 0, v_v)", []));
1.74
1.75 @@ -852,7 +852,7 @@
1.76 (["squareroot","univariate","equation","test"],
1.77 [("#Given" ,["equality e_e","solveFor v_v"]),
1.78 ("#Where" ,["contains_root (e_e::bool)"]),
1.79 - ("#Find" ,["solutions v'i'"])
1.80 + ("#Find" ,["solutions v_v'i'"])
1.81 ],
1.82 append_rls "contains_root" e_rls [Calc ("Test.contains'_root",
1.83 eval_contains_root "#contains_root_")],
1.84 @@ -863,7 +863,7 @@
1.85 (["normalize","univariate","equation","test"],
1.86 [("#Given" ,["equality e_e","solveFor v_v"]),
1.87 ("#Where" ,[]),
1.88 - ("#Find" ,["solutions v'i'"])
1.89 + ("#Find" ,["solutions v_v'i'"])
1.90 ],
1.91 e_rls, SOME "solve (e_e::bool, v_v)", [["Test","norm_univar_equation"]]));
1.92
1.93 @@ -872,7 +872,7 @@
1.94 (["sqroot-test","univariate","equation","test"],
1.95 [("#Given" ,["equality e_e","solveFor v_v"]),
1.96 (*("#Where" ,["contains_root (e_e::bool)"]),*)
1.97 - ("#Find" ,["solutions v'i'"])
1.98 + ("#Find" ,["solutions v_v'i'"])
1.99 ],
1.100 e_rls, SOME "solve (e_e::bool, v_v)", []));
1.101
1.102 @@ -889,7 +889,7 @@
1.103 (["Test","sqrt-equ-test"]:metID,
1.104 [("#Given" ,["equality e_e","solveFor v_v"]),
1.105 ("#Where" ,["contains_root (e_e::bool)"]),
1.106 - ("#Find" ,["solutions v'i'"])
1.107 + ("#Find" ,["solutions v_v'i'"])
1.108 ],
1.109 {rew_ord'="e_rew_ord",rls'=tval_rls,
1.110 srls =append_rls "srls_contains_root" e_rls
1.111 @@ -923,7 +923,7 @@
1.112 (*root-equation ... for test-*.sml until 8.01*)
1.113 (["Test","squ-equ-test2"]:metID,
1.114 [("#Given" ,["equality e_e","solveFor v_v"]),
1.115 - ("#Find" ,["solutions v'i'"])
1.116 + ("#Find" ,["solutions v_v'i'"])
1.117 ],
1.118 {rew_ord'="e_rew_ord",rls'=tval_rls,
1.119 srls = append_rls "srls_contains_root" e_rls
1.120 @@ -957,7 +957,7 @@
1.121 (*tests subproblem fixed linear*)
1.122 (["Test","squ-equ-test-subpbl1"]:metID,
1.123 [("#Given" ,["equality e_e","solveFor v_v"]),
1.124 - ("#Find" ,["solutions v'i'"])
1.125 + ("#Find" ,["solutions v_v'i'"])
1.126 ],
1.127 {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
1.128 crls=tval_rls, nrls=Test_simplify},
1.129 @@ -978,7 +978,7 @@
1.130 (*tests subproblem fixed degree 2*)
1.131 (["Test","squ-equ-test-subpbl2"]:metID,
1.132 [("#Given" ,["equality e_e","solveFor v_v"]),
1.133 - ("#Find" ,["solutions v'i'"])
1.134 + ("#Find" ,["solutions v_v'i'"])
1.135 ],
1.136 {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
1.137 crls=tval_rls, nrls=e_rls(*,
1.138 @@ -998,7 +998,7 @@
1.139 (*root-equation: see foils..., but notTerminating*)
1.140 (["Test","square_equation...notTerminating"]:metID,
1.141 [("#Given" ,["equality e_e","solveFor v_v"]),
1.142 - ("#Find" ,["solutions v'i'"])
1.143 + ("#Find" ,["solutions v_v'i'"])
1.144 ],
1.145 {rew_ord'="e_rew_ord",rls'=tval_rls,
1.146 srls = append_rls "srls_contains_root" e_rls
1.147 @@ -1031,7 +1031,7 @@
1.148 (*root-equation1:*)
1.149 (["Test","square_equation1"]:metID,
1.150 [("#Given" ,["equality e_e","solveFor v_v"]),
1.151 - ("#Find" ,["solutions v'i'"])
1.152 + ("#Find" ,["solutions v_v'i'"])
1.153 ],
1.154 {rew_ord'="e_rew_ord",rls'=tval_rls,
1.155 srls = append_rls "srls_contains_root" e_rls
1.156 @@ -1063,7 +1063,7 @@
1.157 (*root-equation2*)
1.158 (["Test","square_equation2"]:metID,
1.159 [("#Given" ,["equality e_e","solveFor v_v"]),
1.160 - ("#Find" ,["solutions v'i'"])
1.161 + ("#Find" ,["solutions v_v'i'"])
1.162 ],
1.163 {rew_ord'="e_rew_ord",rls'=tval_rls,
1.164 srls = append_rls "srls_contains_root" e_rls
1.165 @@ -1096,7 +1096,7 @@
1.166 (*root-equation*)
1.167 (["Test","square_equation"]:metID,
1.168 [("#Given" ,["equality e_e","solveFor v_v"]),
1.169 - ("#Find" ,["solutions v'i'"])
1.170 + ("#Find" ,["solutions v_v'i'"])
1.171 ],
1.172 {rew_ord'="e_rew_ord",rls'=tval_rls,
1.173 srls = append_rls "srls_contains_root" e_rls
1.174 @@ -1133,7 +1133,7 @@
1.175 "(matches ( ?b*v_v ^^^2 = 0) e_e) |" ^
1.176 "(matches (?a + v_v ^^^2 = 0) e_e) |" ^
1.177 "(matches ( v_v ^^^2 = 0) e_e)"]),
1.178 - ("#Find" ,["solutions v'i'"])
1.179 + ("#Find" ,["solutions v_v'i'"])
1.180 ],
1.181 {rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=e_rls,
1.182 prls = assoc_rls "matches",
1.183 @@ -1155,7 +1155,7 @@
1.184 (["Test","norm_univar_equation"]:metID,
1.185 [("#Given",["equality e_e","solveFor v_v"]),
1.186 ("#Where" ,[]),
1.187 - ("#Find" ,["solutions v'i'"])
1.188 + ("#Find" ,["solutions v_v'i'"])
1.189 ],
1.190 {rew_ord'="e_rew_ord",rls'=tval_rls,srls = e_rls,prls=e_rls,
1.191 calc=[],