test/Tools/isac/Interpret/inform.sml
branchisac-update-Isa09-2
changeset 38058 ad0485155c0e
parent 38050 4c52ad406c20
child 38083 a1d13f3de312
     1.1 --- a/test/Tools/isac/Interpret/inform.sml	Mon Oct 11 12:55:40 2010 +0200
     1.2 +++ b/test/Tools/isac/Interpret/inform.sml	Mon Oct 11 13:31:22 2010 +0200
     1.3 @@ -51,7 +51,7 @@
     1.4  
     1.5   states:=[];
     1.6   CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"], 
     1.7 -	    ("Test.thy", 
     1.8 +	    ("Test", 
     1.9  	     ["sqroot-test","univariate","equation","test"],
    1.10  	     ["Test","squ-equ-test-subpbl1"]))];
    1.11   Iterator 1; moveActiveRoot 1;
    1.12 @@ -124,7 +124,7 @@
    1.13  "--------- appendFormula: on Frm + equ_nrls ----------------------";
    1.14   states:=[];
    1.15   CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"], 
    1.16 -	    ("Test.thy", 
    1.17 +	    ("Test", 
    1.18  	     ["sqroot-test","univariate","equation","test"],
    1.19  	     ["Test","squ-equ-test-subpbl1"]))];
    1.20   Iterator 1; moveActiveRoot 1;
    1.21 @@ -161,7 +161,7 @@
    1.22  "--------- appendFormula: on Res + NO deriv ----------------------";
    1.23   states:=[];
    1.24   CalcTree [(["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 @@ -192,7 +192,7 @@
    1.31  "--------- appendFormula: on Res + late deriv --------------------";
    1.32   states:=[];
    1.33   CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"], 
    1.34 -	    ("Test.thy", 
    1.35 +	    ("Test", 
    1.36  	     ["sqroot-test","univariate","equation","test"],
    1.37  	     ["Test","squ-equ-test-subpbl1"]))];
    1.38   Iterator 1; moveActiveRoot 1;
    1.39 @@ -223,7 +223,7 @@
    1.40  "--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
    1.41   states:=[];
    1.42   CalcTree [(["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 @@ -249,7 +249,7 @@
    1.49  "--------- replaceFormula: on Res + = ----------------------------";
    1.50   states:=[];
    1.51   CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"], 
    1.52 -	    ("Test.thy", 
    1.53 +	    ("Test", 
    1.54  	     ["sqroot-test","univariate","equation","test"],
    1.55  	     ["Test","squ-equ-test-subpbl1"]))];
    1.56   Iterator 1; moveActiveRoot 1;
    1.57 @@ -275,7 +275,7 @@
    1.58  "--------- replaceFormula: on Res + = 1st Nd ---------------------";
    1.59   states:=[];
    1.60   CalcTree [(["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 @@ -300,7 +300,7 @@
    1.67  "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
    1.68   states:=[];
    1.69   CalcTree [(["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 @@ -324,7 +324,7 @@
    1.76  "--------- replaceFormula: cut calculation -----------------------";
    1.77   states:=[];
    1.78   CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"], 
    1.79 -	    ("Test.thy", 
    1.80 +	    ("Test", 
    1.81  	     ["sqroot-test","univariate","equation","test"],
    1.82  	     ["Test","squ-equ-test-subpbl1"]))];
    1.83   Iterator 1; moveActiveRoot 1;
    1.84 @@ -360,7 +360,7 @@
    1.85  	      "interval {x::real. 0 <= x & x <= pi}",
    1.86  	      "errorBound (eps=(0::real))"]
    1.87   (*specifying is not interesting for this example*)
    1.88 - val spec = ("DiffApp.thy", ["maximum_of","function"], 
    1.89 + val spec = ("DiffApp", ["maximum_of","function"], 
    1.90  	     ["DiffApp","max_by_calculus"]);
    1.91   (*the empty model with descriptions for user-guidance by Model_Problem*)
    1.92   val empty_model = [Given ["fixedValues []"],
    1.93 @@ -422,7 +422,7 @@
    1.94  "--------- syntax error ------------------------------------------";
    1.95   states:=[];
    1.96   CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"], 
    1.97 -	    ("Test.thy", 
    1.98 +	    ("Test", 
    1.99  	     ["sqroot-test","univariate","equation","test"],
   1.100  	     ["Test","squ-equ-test-subpbl1"]))];
   1.101   Iterator 1; moveActiveRoot 1;
   1.102 @@ -472,7 +472,7 @@
   1.103  "--------- inform [rational,simplification] ----------------------";
   1.104  states:=[];
   1.105  CalcTree [(["TERM (4/x - 3/y - 1)", "normalform N"],
   1.106 -	   ("Rational.thy",["rational","simplification"],
   1.107 +	   ("Rational",["rational","simplification"],
   1.108  	    ["simplification","of_rationals"]))];
   1.109  Iterator 1; moveActiveRoot 1;
   1.110  autoCalculate 1 CompleteCalcHead;