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