# HG changeset patch # User Walther Neuper # Date 1285224866 -7200 # Node ID f57ddfd09474355e58bb91a224ce69a26bb759e0 # Parent 3147f2c1525c2115364c4a32fad03943ae67be9f tuned pbt's due to copy_named diff -r 3147f2c1525c -r f57ddfd09474 src/Tools/isac/Interpret/calchead.sml --- a/src/Tools/isac/Interpret/calchead.sml Thu Sep 23 08:43:36 2010 +0200 +++ b/src/Tools/isac/Interpret/calchead.sml Thu Sep 23 08:54:26 2010 +0200 @@ -928,7 +928,6 @@ of a SubProblem ? see ME/ptyps.sml 'type met '.*) fun is_copy_named_idstr str = case (rev o explode) str of - (*"_":: _ ::"_"::_ => true*) "'":: _ ::"'"::_ => (tracing ((strs2str o (rev o explode)) "is_copy_named_idstr: " ^ str ^ " T"); true) | _ => (tracing ((strs2str o (rev o explode)) @@ -939,7 +938,6 @@ fun is_copy_named_generating_idstr str = if is_copy_named_idstr str then case (rev o explode) str of - (*"_"::"_"::"_"::_ => false*) "'"::"'"::"'"::_ => false | _ => true else false; @@ -1007,7 +1005,8 @@ (* generate a new variable "x_i" name from a related given one "x" by use of oris relating "v_v'i'" (is_copy_named!) to "v_v" - e.g. (v_v, x) & (v_v'i', ?) --> (v_v'i', x_i) *) + e.g. (v_v, x) & (v_v'i', ?) --> (v_v'i', x_i), + but leave is_copy_named_generating as is, e.t. ss''' *) fun cpy_nam (pbt:pat list) (oris:preori list) (p as (field,(dsc,t)):pat) = (if is_copy_named_generating p then (*WN051014 kept strange old code ...*) diff -r 3147f2c1525c -r f57ddfd09474 src/Tools/isac/Knowledge/Equation.thy --- a/src/Tools/isac/Knowledge/Equation.thy Thu Sep 23 08:43:36 2010 +0200 +++ b/src/Tools/isac/Knowledge/Equation.thy Thu Sep 23 08:54:26 2010 +0200 @@ -44,7 +44,7 @@ (["equation"], [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["matches (?a = ?b) e_e"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], append_rls "equation_prls" e_rls [Calc ("Tools.matches",eval_matches "")], @@ -56,7 +56,7 @@ (["univariate","equation"], [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["matches (?a = ?b) e_e"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], univariate_equation_prls,SOME "solve (e_e::bool, v_v)",[])); diff -r 3147f2c1525c -r f57ddfd09474 src/Tools/isac/Knowledge/LinEq.thy --- a/src/Tools/isac/Knowledge/LinEq.thy Thu Sep 23 08:43:36 2010 +0200 +++ b/src/Tools/isac/Knowledge/LinEq.thy Thu Sep 23 08:54:26 2010 +0200 @@ -134,7 +134,7 @@ "Not( (rhs e_e) is_polyrat_in v_v)", "((lhs e_e) has_degree_in v_v)=1", "((rhs e_e) has_degree_in v_v)=1"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], LinEq_prls, SOME "solve (e_e::bool, v_v)", [["LinEq","solve_lineq_equation"]])); @@ -155,7 +155,7 @@ [("#Given", ["equality e_e", "solveFor v_v"]), ("#Where", ["Not ((lhs e_e) is_polyrat_in v_v)", "((lhs e_e) has_degree_in v_v) = 1"]), - ("#Find", ["solutions v'i'"]) + ("#Find", ["solutions v_v'i'"]) ], {rew_ord'="termlessI", rls'=LinEq_erls, srls=e_rls, prls=LinEq_prls, calc=[], crls=LinEq_crls, nrls=norm_Poly}, diff -r 3147f2c1525c -r f57ddfd09474 src/Tools/isac/Knowledge/LogExp.thy --- a/src/Tools/isac/Knowledge/LogExp.thy Thu Sep 23 08:43:36 2010 +0200 +++ b/src/Tools/isac/Knowledge/LogExp.thy Thu Sep 23 08:54:26 2010 +0200 @@ -33,7 +33,7 @@ (["logarithmic","univariate","equation"], [("#Given",["equality e_e","solveFor v_v"]), ("#Where",["matches ((?a log ?v_v) = ?b) e_e"]), - ("#Find" ,["solutions v'i'"]), + ("#Find" ,["solutions v_v'i'"]), ("#With" ,["||(lhs (Subst (v'i', v_v) e_e) - " ^ " (rhs (Subst (v'i', v_v) e_e) || < eps)"]) ], @@ -47,7 +47,7 @@ (["Equation","solve_log"], [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["matches ((?a log ?v_v) = ?b) e_e"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls, calc=[],crls=PolyEq_crls, nrls=norm_Rational}, diff -r 3147f2c1525c -r f57ddfd09474 src/Tools/isac/Knowledge/PolyEq.thy --- a/src/Tools/isac/Knowledge/PolyEq.thy Thu Sep 23 08:43:36 2010 +0200 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Thu Sep 23 08:54:26 2010 +0200 @@ -849,7 +849,7 @@ ("#Where" ,["~((e_e::bool) is_ratequation_in (v_v::real))", "~((lhs e_e) is_rootTerm_in (v_v::real))", "~((rhs e_e) is_rootTerm_in (v_v::real))"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], PolyEq_prls, SOME "solve (e_e::bool, v_v)", [])); @@ -862,7 +862,7 @@ "(lhs e_e) is_poly_in v_v", "((lhs e_e) has_degree_in v_v ) = 0" ]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d0_polyeq_equation"]])); @@ -876,7 +876,7 @@ "(lhs e_e) is_poly_in v_v", "((lhs e_e) has_degree_in v_v ) = 1" ]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d1_polyeq_equation"]])); @@ -890,7 +890,7 @@ ("#Where" ,["matches (?a = 0) e_e", "(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v ) = 2"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d2_polyeq_equation"]])); @@ -911,7 +911,7 @@ "Not (matches ( ?b*?v_ + ?v_^^^2 = 0) e_e) &" ^ "Not (matches ( ?v_ + ?c*?v_^^^2 = 0) e_e) &" ^ "Not (matches ( ?b*?v_ + ?c*?v_^^^2 = 0) e_e)"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d2_polyeq_sqonly_equation"]])); @@ -926,7 +926,7 @@ "matches (?a*?v_ + ?b*?v_^^^2 = 0) e_e | " ^ "matches ( ?v_^^^2 = 0) e_e | " ^ "matches ( ?b*?v_^^^2 = 0) e_e "]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d2_polyeq_bdvonly_equation"]])); @@ -937,7 +937,7 @@ [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["matches (?a + 1*?v_^^^2 = 0) e_e | " ^ "matches (?a + ?v_^^^2 = 0) e_e"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d2_polyeq_pq_equation"]])); @@ -948,7 +948,7 @@ [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["matches (?a + ?v_^^^2 = 0) e_e | " ^ "matches (?a + ?b*?v_^^^2 = 0) e_e"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d2_polyeq_abc_equation"]])); @@ -962,7 +962,7 @@ ("#Where" ,["matches (?a = 0) e_e", "(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 3"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d3_polyeq_equation"]])); @@ -975,7 +975,7 @@ ("#Where" ,["matches (?a = 0) e_e", "(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 4"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], PolyEq_prls, SOME "solve (e_e::bool, v_v)", [(*["PolyEq","solve_d4_polyeq_equation"]*)])); @@ -987,7 +987,7 @@ [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["(Not((matches (?a = 0 ) e_e ))) |" ^ "(Not(((lhs e_e) is_poly_in v_v)))"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","normalize_poly"]])); @@ -998,7 +998,7 @@ [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["matches (?a = 0) e_e", "(lhs e_e) is_expanded_in v_v "]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], PolyEq_prls, SOME "solve (e_e::bool, v_v)", [])); @@ -1009,7 +1009,7 @@ (["degree_2","expanded","univariate","equation"], [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["((lhs e_e) has_degree_in v_v) = 2"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","complete_square"]])); @@ -1043,7 +1043,7 @@ [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["(Not((matches (?a = 0 ) e_e ))) |" ^ "(Not(((lhs e_e) is_poly_in v_v)))"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], {rew_ord'="termlessI", rls'=PolyEq_erls, @@ -1070,7 +1070,7 @@ [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 0"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], {rew_ord'="termlessI", rls'=PolyEq_erls, @@ -1091,7 +1091,7 @@ [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 1"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], {rew_ord'="termlessI", rls'=PolyEq_erls, srls=e_rls, prls=PolyEq_prls, calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], @@ -1112,7 +1112,7 @@ [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], {rew_ord'="termlessI", rls'=PolyEq_erls, @@ -1139,7 +1139,7 @@ [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], {rew_ord'="termlessI", rls'=PolyEq_erls, @@ -1166,7 +1166,7 @@ [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], {rew_ord'="termlessI", rls'=PolyEq_erls, @@ -1190,7 +1190,7 @@ [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], {rew_ord'="termlessI", rls'=PolyEq_erls, @@ -1214,7 +1214,7 @@ [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], {rew_ord'="termlessI", rls'=PolyEq_erls, @@ -1238,7 +1238,7 @@ [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 3"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], {rew_ord'="termlessI", rls'=PolyEq_erls, @@ -1271,7 +1271,7 @@ [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["matches (?a = 0) e_e", "((lhs e_e) has_degree_in v_v) = 2"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls, calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], diff -r 3147f2c1525c -r f57ddfd09474 src/Tools/isac/Knowledge/RatEq.thy --- a/src/Tools/isac/Knowledge/RatEq.thy Thu Sep 23 08:43:36 2010 +0200 +++ b/src/Tools/isac/Knowledge/RatEq.thy Thu Sep 23 08:54:26 2010 +0200 @@ -175,7 +175,7 @@ (["rational","univariate","equation"], [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["(e_e::bool) is_ratequation_in (v_v::real)"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], RatEq_prls, SOME "solve (e_e::bool, v_v)", @@ -199,7 +199,7 @@ (["RatEq","solve_rat_equation"], [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["(e_e::bool) is_ratequation_in (v_v::real)"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], {rew_ord'="termlessI", rls'=rateq_erls, diff -r 3147f2c1525c -r f57ddfd09474 src/Tools/isac/Knowledge/RootEq.thy --- a/src/Tools/isac/Knowledge/RootEq.thy Thu Sep 23 08:43:36 2010 +0200 +++ b/src/Tools/isac/Knowledge/RootEq.thy Thu Sep 23 08:54:26 2010 +0200 @@ -482,7 +482,7 @@ [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["(lhs e_e) is_rootTerm_in (v_v::real) | " ^ "(rhs e_e) is_rootTerm_in (v_v::real)"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], RootEq_prls, SOME "solve (e_e::bool, v_v)", [])); @@ -495,7 +495,7 @@ " ((lhs e_e) is_normSqrtTerm_in (v_v::real)) ) |" ^ "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ " ((rhs e_e) is_normSqrtTerm_in (v_v::real)) )"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], RootEq_prls, SOME "solve (e_e::bool, v_v)", [["RootEq","solve_sq_root_equation"]])); @@ -508,7 +508,7 @@ " Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) | " ^ "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ " Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], RootEq_prls, SOME "solve (e_e::bool, v_v)", [["RootEq","norm_sq_root_equation"]])); @@ -532,7 +532,7 @@ " Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) | " ^ "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ " Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], {rew_ord'="termlessI", rls'=RootEq_erls, srls=e_rls, prls=RootEq_prls, calc=[], crls=RootEq_crls, nrls=norm_Poly}, @@ -558,7 +558,7 @@ " ((lhs e_e) is_normSqrtTerm_in (v_v::real))) |" ^ "(((rhs e_e) is_sqrtTerm_in (v_v::real)) & " ^ " ((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], {rew_ord'="termlessI", rls'=RootEq_erls, srls = rooteq_srls, prls = RootEq_prls, calc = [], crls=RootEq_crls, nrls=norm_Poly}, @@ -586,7 +586,7 @@ (["RootEq","solve_right_sq_root_equation"], [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["(rhs e_e) is_sqrtTerm_in v_v"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], {rew_ord' = "termlessI", rls' = RootEq_erls, srls = e_rls, prls = RootEq_prls, calc = [], crls = RootEq_crls, nrls = norm_Poly}, @@ -611,7 +611,7 @@ (["RootEq","solve_left_sq_root_equation"], [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["(lhs e_e) is_sqrtTerm_in v_v"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], {rew_ord'="termlessI", rls'=RootEq_erls, diff -r 3147f2c1525c -r f57ddfd09474 src/Tools/isac/Knowledge/RootRatEq.thy --- a/src/Tools/isac/Knowledge/RootRatEq.thy Thu Sep 23 08:43:36 2010 +0200 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Thu Sep 23 08:54:26 2010 +0200 @@ -144,7 +144,7 @@ [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) )| " ^ "( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], RootRatEq_prls, SOME "solve (e_e::bool, v_v)", [["RootRatEq","elim_rootrat_equation"]])); @@ -164,7 +164,7 @@ [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) ) | " ^ "( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], {rew_ord'="termlessI", rls'=RooRatEq_erls, diff -r 3147f2c1525c -r f57ddfd09474 src/Tools/isac/Knowledge/Test.thy --- a/src/Tools/isac/Knowledge/Test.thy Thu Sep 23 08:43:36 2010 +0200 +++ b/src/Tools/isac/Knowledge/Test.thy Thu Sep 23 08:54:26 2010 +0200 @@ -522,7 +522,7 @@ (["equation","test"], [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["matches (?a = ?b) e_e"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], assoc_rls "matches", SOME "solve (e_e::bool, v_v)", [])); @@ -543,7 +543,7 @@ [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["(matches ( v_v = 0) e_e) | (matches ( ?b*v_v = 0) e_e) |" ^ "(matches (?a+v_v = 0) e_e) | (matches (?a+?b*v_v = 0) e_e) "]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], assoc_rls "matches", SOME "solve (e_e::bool, v_v)", [["Test","solve_linear"]])); @@ -595,7 +595,7 @@ (["Test","solve_linear"]:metID, [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["matches (?a = ?b) e_e"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls, prls = assoc_rls "matches", calc = [], crls = tval_rls, @@ -783,7 +783,7 @@ "(matches ( ?b*v_v ^^^2 = 0) e_e) |" ^ "(matches (?a + v_v ^^^2 = 0) e_e) |" ^ "(matches ( v_v ^^^2 = 0) e_e)"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], assoc_rls "matches", SOME "solve (e_e::bool, v_v)", [["Test","solve_plain_square"]])); @@ -817,7 +817,7 @@ (["polynomial","univariate","equation","test"], [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]), ("#Where" ,["False"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], e_rls, SOME "solve (e_e::bool, v_v)", [])); @@ -825,7 +825,7 @@ (prep_pbt thy "pbl_test_uni_poly_deg2" [] e_pblID (["degree_two","polynomial","univariate","equation","test"], [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", [])); @@ -833,7 +833,7 @@ (prep_pbt thy "pbl_test_uni_poly_deg2_pq" [] e_pblID (["pq_formula","degree_two","polynomial","univariate","equation","test"], [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", [])); @@ -841,7 +841,7 @@ (prep_pbt thy "pbl_test_uni_poly_deg2_abc" [] e_pblID (["abc_formula","degree_two","polynomial","univariate","equation","test"], [("#Given" ,["equality (a_a * x ^^^2 + b_b * x + c_c = 0)","solveFor v_v"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], e_rls, SOME "solve (a_a * x ^^^2 + b_b * x + c_c = 0, v_v)", [])); @@ -852,7 +852,7 @@ (["squareroot","univariate","equation","test"], [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["contains_root (e_e::bool)"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], append_rls "contains_root" e_rls [Calc ("Test.contains'_root", eval_contains_root "#contains_root_")], @@ -863,7 +863,7 @@ (["normalize","univariate","equation","test"], [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,[]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], e_rls, SOME "solve (e_e::bool, v_v)", [["Test","norm_univar_equation"]])); @@ -872,7 +872,7 @@ (["sqroot-test","univariate","equation","test"], [("#Given" ,["equality e_e","solveFor v_v"]), (*("#Where" ,["contains_root (e_e::bool)"]),*) - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], e_rls, SOME "solve (e_e::bool, v_v)", [])); @@ -889,7 +889,7 @@ (["Test","sqrt-equ-test"]:metID, [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["contains_root (e_e::bool)"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], {rew_ord'="e_rew_ord",rls'=tval_rls, srls =append_rls "srls_contains_root" e_rls @@ -923,7 +923,7 @@ (*root-equation ... for test-*.sml until 8.01*) (["Test","squ-equ-test2"]:metID, [("#Given" ,["equality e_e","solveFor v_v"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], {rew_ord'="e_rew_ord",rls'=tval_rls, srls = append_rls "srls_contains_root" e_rls @@ -957,7 +957,7 @@ (*tests subproblem fixed linear*) (["Test","squ-equ-test-subpbl1"]:metID, [("#Given" ,["equality e_e","solveFor v_v"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[], crls=tval_rls, nrls=Test_simplify}, @@ -978,7 +978,7 @@ (*tests subproblem fixed degree 2*) (["Test","squ-equ-test-subpbl2"]:metID, [("#Given" ,["equality e_e","solveFor v_v"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[], crls=tval_rls, nrls=e_rls(*, @@ -998,7 +998,7 @@ (*root-equation: see foils..., but notTerminating*) (["Test","square_equation...notTerminating"]:metID, [("#Given" ,["equality e_e","solveFor v_v"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], {rew_ord'="e_rew_ord",rls'=tval_rls, srls = append_rls "srls_contains_root" e_rls @@ -1031,7 +1031,7 @@ (*root-equation1:*) (["Test","square_equation1"]:metID, [("#Given" ,["equality e_e","solveFor v_v"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], {rew_ord'="e_rew_ord",rls'=tval_rls, srls = append_rls "srls_contains_root" e_rls @@ -1063,7 +1063,7 @@ (*root-equation2*) (["Test","square_equation2"]:metID, [("#Given" ,["equality e_e","solveFor v_v"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], {rew_ord'="e_rew_ord",rls'=tval_rls, srls = append_rls "srls_contains_root" e_rls @@ -1096,7 +1096,7 @@ (*root-equation*) (["Test","square_equation"]:metID, [("#Given" ,["equality e_e","solveFor v_v"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], {rew_ord'="e_rew_ord",rls'=tval_rls, srls = append_rls "srls_contains_root" e_rls @@ -1133,7 +1133,7 @@ "(matches ( ?b*v_v ^^^2 = 0) e_e) |" ^ "(matches (?a + v_v ^^^2 = 0) e_e) |" ^ "(matches ( v_v ^^^2 = 0) e_e)"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], {rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=e_rls, prls = assoc_rls "matches", @@ -1155,7 +1155,7 @@ (["Test","norm_univar_equation"]:metID, [("#Given",["equality e_e","solveFor v_v"]), ("#Where" ,[]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], {rew_ord'="e_rew_ord",rls'=tval_rls,srls = e_rls,prls=e_rls, calc=[], diff -r 3147f2c1525c -r f57ddfd09474 test/Tools/isac/Test_Isac.thy --- a/test/Tools/isac/Test_Isac.thy Thu Sep 23 08:43:36 2010 +0200 +++ b/test/Tools/isac/Test_Isac.thy Thu Sep 23 08:54:26 2010 +0200 @@ -77,9 +77,9 @@ use"complex.sml"; use"diff.sml"; use"diffapp.sml"; -*) +(**) use"Knowledge/integrate.sml"; -(* +(**) use"equation.sml"; (*use"inssort.sml"; problems with recdef in Isabelle2002*) use"logexp.sml";