test/Tools/isac/Interpret/me.sml
branchisac-update-Isa09-2
changeset 38058 ad0485155c0e
parent 38043 6a36acec95d9
child 42124 ba52b628c40c
     1.1 --- a/test/Tools/isac/Interpret/me.sml	Mon Oct 11 12:55:40 2010 +0200
     1.2 +++ b/test/Tools/isac/Interpret/me.sml	Mon Oct 11 13:31:22 2010 +0200
     1.3 @@ -32,7 +32,7 @@
     1.4  CalcTree
     1.5  [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
     1.6  	   "solveFor x","solutions L"], 
     1.7 -  ("RatEq.thy",["univariate","equation"],["no_met"]))];
     1.8 +  ("RatEq",["univariate","equation"],["no_met"]))];
     1.9  Iterator 1; moveActiveRoot 1;
    1.10  autoCalculate 1 CompleteCalc; 
    1.11  
    1.12 @@ -226,7 +226,7 @@
    1.13  CalcTree
    1.14  [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
    1.15  	   "solveFor x","solutions L"], 
    1.16 -  ("RatEq.thy",["univariate","equation"],["no_met"]))];
    1.17 +  ("RatEq",["univariate","equation"],["no_met"]))];
    1.18  Iterator 1; moveActiveRoot 1;
    1.19  autoCalculate 1 CompleteCalc; 
    1.20  val ((pt,_),_) = get_calc 1;
    1.21 @@ -338,7 +338,7 @@
    1.22   val c = [];
    1.23   val (p,_,f,nxt,_,pt) = CalcTreeTEST 
    1.24       [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
    1.25 -       ("Test.thy", 
    1.26 +       ("Test", 
    1.27  	["linear","univariate","equation","test"],
    1.28  	["Test","solve_linear"]))];
    1.29   val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.30 @@ -374,7 +374,7 @@
    1.31   states:=[];
    1.32   CalcTree      (*start of calculation, return No.1*)
    1.33       [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
    1.34 -       ("Test.thy", 
    1.35 +       ("Test", 
    1.36  	["linear","univariate","equation","test"],
    1.37  	["Test","solve_linear"]))];
    1.38   Iterator 1; moveActiveRoot 1;
    1.39 @@ -421,7 +421,7 @@
    1.40  	"interval {x::real. 0 <= x & x <= 2*r}",
    1.41  	"interval {x::real. 0 <= x & x <= pi}",
    1.42  	"errorBound (eps=(0::real))"],
    1.43 -       ("DiffApp.thy",["maximum_of","function"],["DiffApp","max_by_calculus"])
    1.44 +       ("DiffApp",["maximum_of","function"],["DiffApp","max_by_calculus"])
    1.45         )];
    1.46   val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.47   val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.48 @@ -430,7 +430,7 @@
    1.49   val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => OldGoals.print_exn e;
    1.50   val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.51   val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.52 - (*nxt = Specify_Theory "DiffApp.thy"*)
    1.53 + (*nxt = Specify_Theory "DiffApp"*)
    1.54   val (oris, _, _) = get_obj g_origin pt (fst p);
    1.55   writeln (oris2str oris);
    1.56  (*[
    1.57 @@ -487,7 +487,7 @@
    1.58  	"interval {x::real. 0 <= x & x <= 2*r}",
    1.59  	"interval {x::real. 0 <= x & x <= pi}",
    1.60  	"errorBound (eps=(0::real))"],
    1.61 -       ("DiffApp.thy",["maximum_of","function"],["DiffApp","max_by_calculus"])
    1.62 +       ("DiffApp",["maximum_of","function"],["DiffApp","max_by_calculus"])
    1.63         )];
    1.64   val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.65   val (p,_,f,nxt,_,pt) = me nxt p c pt;