1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Wed Sep 08 16:45:27 2010 +0200
1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Wed Sep 08 16:47:22 2010 +0200
1.3 @@ -252,7 +252,7 @@
1.4 states:=[];
1.5 CalcTree [(["TERM (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",
1.6 "normalform N"],
1.7 - ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"],
1.8 + ("PolyMinus",["plus_minus","polynom","vereinfachen"],
1.9 ["simplification","for_polynomials","with_minus"]))];
1.10 moveActiveRoot 1;
1.11 autoCalculate 1 CompleteCalc;
1.12 @@ -265,7 +265,7 @@
1.13 states:=[];
1.14 CalcTree [(["TERM (-r - 2*s - 3*t + 5 + 4*r + 8*s - 5*t - 2)",
1.15 "normalform N"],
1.16 - ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"],
1.17 + ("PolyMinus",["plus_minus","polynom","vereinfachen"],
1.18 ["simplification","for_polynomials","with_minus"]))];
1.19 moveActiveRoot 1;
1.20 autoCalculate 1 CompleteCalc;
1.21 @@ -279,7 +279,7 @@
1.22 states:=[];
1.23 CalcTree [(["TERM (3*e - 6*f - 8*e - 4*f + 5*e + 7*f)",
1.24 "normalform N"],
1.25 - ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"],
1.26 + ("PolyMinus",["plus_minus","polynom","vereinfachen"],
1.27 ["simplification","for_polynomials","with_minus"]))];
1.28 moveActiveRoot 1;
1.29 autoCalculate 1 CompleteCalc;
1.30 @@ -292,7 +292,7 @@
1.31 states:=[];
1.32 CalcTree [(["TERM (8*u - 5*v - 5*u + 7*v - 6*u - 3*v)",
1.33 "normalform N"],
1.34 - ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"],
1.35 + ("PolyMinus",["plus_minus","polynom","vereinfachen"],
1.36 ["simplification","for_polynomials","with_minus"]))];
1.37 moveActiveRoot 1;
1.38 autoCalculate 1 CompleteCalc;
1.39 @@ -305,7 +305,7 @@
1.40 states:=[];
1.41 CalcTree [(["TERM (2*u - 3*v - 6*u + 5*v)",
1.42 "normalform N"],
1.43 - ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"],
1.44 + ("PolyMinus",["plus_minus","polynom","vereinfachen"],
1.45 ["simplification","for_polynomials","with_minus"]))];
1.46 moveActiveRoot 1;
1.47 autoCalculate 1 CompleteCalc;
1.48 @@ -320,7 +320,7 @@
1.49 "----------- met probe fuer_polynom ------------------------------";
1.50 val str =
1.51 "Script ProbeScript (e_e::bool) (ws_::bool list) =\
1.52 -\ (let e_e = Take e_; \
1.53 +\ (let e_e = Take e_e; \
1.54 \ e_e = Substitute ws_ e_e \
1.55 \ in (Repeat((Try (Repeat (Calculate TIMES))) @@ \
1.56 \ (Try (Repeat (Calculate PLUS ))) @@ \
1.57 @@ -337,7 +337,7 @@
1.58 \3 - 2 * e + 2 * f + 2 * g)",
1.59 "mitWert [e = 1, f = 2, g = 3]",
1.60 "Geprueft b"],
1.61 - ("PolyMinus.thy",["polynom","probe"],
1.62 + ("PolyMinus",["polynom","probe"],
1.63 ["probe","fuer_polynom"]))];
1.64 moveActiveRoot 1;
1.65 autoCalculate 1 CompleteCalc;
1.66 @@ -359,7 +359,7 @@
1.67 states:=[];
1.68 CalcTree [(["TERM (2*u - 5 - (3 - 4*u) + (8*u + 9))",
1.69 "normalform N"],
1.70 - ("PolyMinus.thy",["klammer","polynom","vereinfachen"],
1.71 + ("PolyMinus",["klammer","polynom","vereinfachen"],
1.72 ["simplification","for_polynomials","with_parentheses"]))];
1.73 moveActiveRoot 1;
1.74 autoCalculate 1 CompleteCalc;
1.75 @@ -374,7 +374,7 @@
1.76 CalcTree [(["Pruefe (2*u - 5 - (3 - 4*u) + (8*u + 9) = 1 + 14 * u)",
1.77 "mitWert [u = 2]",
1.78 "Geprueft b"],
1.79 - ("PolyMinus.thy",["polynom","probe"],
1.80 + ("PolyMinus",["polynom","probe"],
1.81 ["probe","fuer_polynom"]))];
1.82 moveActiveRoot 1;
1.83 autoCalculate 1 CompleteCalc;
1.84 @@ -390,7 +390,7 @@
1.85 states:=[];
1.86 CalcTree [(["TERM (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",
1.87 "normalform N"],
1.88 - ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"],
1.89 + ("PolyMinus",["plus_minus","polynom","vereinfachen"],
1.90 ["simplification","for_polynomials","with_minus"]))];
1.91 moveActiveRoot 1;
1.92 autoCalculate 1 CompleteCalcHead;
1.93 @@ -450,7 +450,7 @@
1.94 states:=[];
1.95 CalcTree [(["TERM (- (8 * g) + 10 * g + h)",
1.96 "normalform N"],
1.97 - ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"],
1.98 + ("PolyMinus",["plus_minus","polynom","vereinfachen"],
1.99 ["simplification","for_polynomials","with_minus"]))];
1.100 moveActiveRoot 1;
1.101 autoCalculate 1 CompleteCalc;
1.102 @@ -462,7 +462,7 @@
1.103 states:=[];
1.104 CalcTree [(["TERM (- (8 * g) + 10 * g + f)",
1.105 "normalform N"],
1.106 - ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"],
1.107 + ("PolyMinus",["plus_minus","polynom","vereinfachen"],
1.108 ["simplification","for_polynomials","with_minus"]))];
1.109 moveActiveRoot 1;
1.110 autoCalculate 1 CompleteCalc;
1.111 @@ -511,7 +511,7 @@
1.112 states:=[];
1.113 CalcTree [(["TERM ((3*a + 2) * (4*a - 1))",
1.114 "normalform N"],
1.115 - ("PolyMinus.thy",["binom_klammer","polynom","vereinfachen"],
1.116 + ("PolyMinus",["binom_klammer","polynom","vereinfachen"],
1.117 ["simplification","for_polynomials","with_parentheses_mult"]))];
1.118 moveActiveRoot 1;
1.119 autoCalculate 1 CompleteCalc;
1.120 @@ -530,7 +530,7 @@
1.121 states:=[];
1.122 CalcTree [(["TERM (8*(a - q) + a - 2*q + 3*(a - 2*q))",
1.123 "normalform N"],
1.124 - ("PolyMinus.thy",["binom_klammer","polynom","vereinfachen"],
1.125 + ("PolyMinus",["binom_klammer","polynom","vereinfachen"],
1.126 ["simplification","for_polynomials","with_parentheses_mult"]))];
1.127 moveActiveRoot 1;
1.128 autoCalculate 1 CompleteCalc;