1.1 --- a/test/Tools/isac/Interpret/ctree.sml	Mon Oct 11 12:55:40 2010 +0200
     1.2 +++ b/test/Tools/isac/Interpret/ctree.sml	Mon Oct 11 13:31:22 2010 +0200
     1.3 @@ -67,7 +67,7 @@
     1.4  val fmz = ["equality (x+1=2)",
     1.5  	   "solveFor x","solutions L"];
     1.6  val (dI',pI',mI') =
     1.7 -  ("Test.thy",["sqroot-test","univariate","equation","test"],
     1.8 +  ("Test",["sqroot-test","univariate","equation","test"],
     1.9     ["Test","squ-equ-test-subpbl1"]);
    1.10  val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    1.11  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.12 @@ -308,7 +308,7 @@
    1.13  val fmz = ["equality (x+1=2)",
    1.14  	   "solveFor x","solutions L"];
    1.15  val (dI',pI',mI') =
    1.16 -  ("Test.thy",["sqroot-test","univariate","equation","test"],
    1.17 +  ("Test",["sqroot-test","univariate","equation","test"],
    1.18     ["Test","squ-equ-test-subpbl1"]);
    1.19  val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    1.20  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.21 @@ -350,7 +350,7 @@
    1.22   states:=[];
    1.23   CalcTree
    1.24   [(["equality (x+1=2)", "solveFor x","solutions L"], 
    1.25 -   ("Test.thy", 
    1.26 +   ("Test", 
    1.27      ["sqroot-test","univariate","equation","test"],
    1.28      ["Test","squ-equ-test-subpbl1"]))];
    1.29   Iterator 1; moveActiveRoot 1;
    1.30 @@ -416,7 +416,7 @@
    1.31  val fmz = ["equality (x+1=2)",
    1.32  	   "solveFor x","solutions L"];
    1.33  val (dI',pI',mI') =
    1.34 -  ("Test.thy",["sqroot-test","univariate","equation","test"],
    1.35 +  ("Test",["sqroot-test","univariate","equation","test"],
    1.36     ["Test","squ-equ-test-subpbl1"]);
    1.37  val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    1.38  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.39 @@ -517,7 +517,7 @@
    1.40   states:=[];
    1.41   CalcTree
    1.42   [(["equality (x+1=2)", "solveFor x","solutions L"], 
    1.43 -   ("Test.thy", 
    1.44 +   ("Test", 
    1.45      ["sqroot-test","univariate","equation","test"],
    1.46      ["Test","squ-equ-test-subpbl1"]))];
    1.47   Iterator 1; moveActiveRoot 1;
    1.48 @@ -554,7 +554,7 @@
    1.49   states := [];
    1.50   CalcTree      (*start of calculation, return No.1*)
    1.51       [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
    1.52 -       ("Test.thy", 
    1.53 +       ("Test", 
    1.54  	["linear","univariate","equation","test"],
    1.55  	["Test","solve_linear"]))];
    1.56   Iterator 1; moveActiveRoot 1;
    1.57 @@ -601,7 +601,7 @@
    1.58   states:=[];
    1.59   CalcTree
    1.60   [(["equality (x+1=2)", "solveFor x","solutions L"], 
    1.61 -   ("Test.thy", 
    1.62 +   ("Test", 
    1.63      ["sqroot-test","univariate","equation","test"],
    1.64      ["Test","squ-equ-test-subpbl1"]))];
    1.65   Iterator 1; moveActiveRoot 1;
    1.66 @@ -635,7 +635,7 @@
    1.67   states:=[];
    1.68   CalcTree
    1.69   [(["equality (x+1=2)", "solveFor x","solutions L"], 
    1.70 -   ("Test.thy", 
    1.71 +   ("Test", 
    1.72      ["sqroot-test","univariate","equation","test"],
    1.73      ["Test","squ-equ-test-subpbl1"]))];
    1.74   Iterator 1; moveActiveRoot 1;
    1.75 @@ -671,7 +671,7 @@
    1.76  CalcTree
    1.77  [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
    1.78  	   "solveFor x","solutions L"], 
    1.79 -  ("RatEq.thy",["univariate","equation"],["no_met"]))];
    1.80 +  ("RatEq",["univariate","equation"],["no_met"]))];
    1.81  Iterator 1; moveActiveRoot 1;
    1.82  autoCalculate 1 CompleteCalc; 
    1.83  
    1.84 @@ -853,7 +853,7 @@
    1.85  CalcTree
    1.86  [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
    1.87  	   "solveFor x","solutions L"], 
    1.88 -  ("RatEq.thy",["univariate","equation"],["no_met"]))];
    1.89 +  ("RatEq",["univariate","equation"],["no_met"]))];
    1.90  Iterator 1; moveActiveRoot 1;
    1.91  autoCalculate 1 CompleteCalc; 
    1.92  val ((pt,_),_) = get_calc 1;
    1.93 @@ -867,7 +867,7 @@
    1.94  case (term2str form, tac, terms2strs asm) of
    1.95      ("(3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)",
    1.96       Subproblem
    1.97 -         ("PolyEq.thy",
    1.98 +         ("PolyEq",
    1.99            ["normalize", "polynomial", "univariate", "equation"]),
   1.100  	 ["9 * x + -6 * x ^^^ 2 + x ^^^ 3 ~= 0"]) => ()
   1.101    | _ => error "diff.behav.in ctree.sml: pt_extract asm<>[]";
   1.102 @@ -877,7 +877,7 @@
   1.103    case (term2str form, tac, terms2strs asm) of
   1.104      ((*"(3 + (-1 * x + x ^^^ 2)) * x = 1 * (9 * x + (x ^^^ 3 + -6 * x ^^^ 2))",
   1.105       *)Subproblem
   1.106 -         ("PolyEq.thy",
   1.107 +         ("PolyEq",
   1.108            ["normalize", "polynomial", "univariate", "equation"]),
   1.109  	 ["9 * x + (x ^^^ 3 + -6 * x ^^^ 2) ~= 0"]) => ()
   1.110    | _ => error "diff.behav.in ctree.sml: pt_extract asm<>[]";
   1.111 @@ -892,7 +892,7 @@
   1.112  states:=[];
   1.113  CalcTree
   1.114   [(["equality (x+1=2)", "solveFor x","solutions L"], 
   1.115 -   ("Test.thy", 
   1.116 +   ("Test", 
   1.117      ["sqroot-test","univariate","equation","test"],
   1.118      ["Test","squ-equ-test-subpbl1"]))];
   1.119  Iterator 1; moveActiveRoot 1;
   1.120 @@ -923,7 +923,7 @@
   1.121  val (Form form, SOME tac, asm) = pt_extract (pt, ([2], Res));
   1.122  case (term2str form, tac, terms2strs asm) of
   1.123      ("-1 + x = 0",
   1.124 -     Subproblem ("Test.thy", ["linear", "univariate", "equation", "test"]),
   1.125 +     Subproblem ("Test", ["linear", "univariate", "equation", "test"]),
   1.126       []) => ()
   1.127    | _ => error "diff.behav.in ctree.sml: pt_extract ([2], Res)";
   1.128  
   1.129 @@ -971,7 +971,7 @@
   1.130  states:=[];
   1.131  CalcTree
   1.132   [(["equality (x+1=2)", "solveFor x","solutions L"], 
   1.133 -   ("Test.thy", 
   1.134 +   ("Test", 
   1.135      ["sqroot-test","univariate","equation","test"],
   1.136      ["Test","squ-equ-test-subpbl1"]))];
   1.137  Iterator 1; moveActiveRoot 1;