1.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml	Mon Oct 11 12:55:40 2010 +0200
     1.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml	Mon Oct 11 13:31:22 2010 +0200
     1.3 @@ -40,7 +40,7 @@
     1.4  " _________________ equation with x =(-12)/5, but L ={} ------- ";
     1.5  (*                  -------------------------------------         *)
     1.6  " _________________ rewrite _________________ ";
     1.7 -val thy' = "Test.thy";
     1.8 +val thy' = "Test";
     1.9  val ct = "sqrt(9+4*x)=sqrt x + sqrt(-3+x)";
    1.10  val thm = ("square_equation_left","");
    1.11  val SOME (ct,asm) = rewrite thy' "tless_true" "tval_rls" true thm ct;
    1.12 @@ -213,7 +213,7 @@
    1.13  atomty ((#prop o rep_thm) (!tthm));
    1.14  atomty (term_of (!tct));
    1.15  *)
    1.16 -val thy' = "Test.thy";
    1.17 +val thy' = "Test";
    1.18  val ct = "sqrt(9+4*x)=sqrt x + sqrt(5+x)";
    1.19  (*1*)val thm = ("square_equation_left","");
    1.20  val (ct,asm) = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
    1.21 @@ -257,7 +257,7 @@
    1.22  " _________________ rewrite + cappend _________________ ";
    1.23  " _________________ rewrite + cappend _________________ ";
    1.24  " _________________ rewrite + cappend _________________ ";
    1.25 -val thy' = "Test.thy";
    1.26 +val thy' = "Test";
    1.27  val ct = str2term"sqrt(9+4*x)=sqrt x + sqrt(5+x)";
    1.28  val ctl = ["sqrt(9+4*x)=sqrt x + sqrt(5+x)","x::real","0"];
    1.29  val oris = prep_ori ctl thy 
    1.30 @@ -400,8 +400,8 @@
    1.31  	   "solutions L"(*,
    1.32        "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < eps}"*)];
    1.33  val (dI',pI',mI') =
    1.34 -  ("Test.thy",["sqroot-test","univariate","equation","test"],
    1.35 -   ("Test.thy","sqrt-equ-test"));
    1.36 +  ("Test",["sqroot-test","univariate","equation","test"],
    1.37 +   ("Test","sqrt-equ-test"));
    1.38  val p = e_pos'; val c = []; 
    1.39  val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
    1.40  
    1.41 @@ -414,15 +414,15 @@
    1.42  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.43  (* val nxt = ("Add_Find",Add_Find "solutions L"); *)
    1.44  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.45 -(* val nxt = ("Specify_Theory",Specify_Theory "DiffAppl.thy");
    1.46 +(* val nxt = ("Specify_Theory",Specify_Theory "DiffAppl");
    1.47  > get_obj g_spec pt (fst p);
    1.48  val it = ("e_domID",["e_pblID"],("e_domID","e_metID")) : spec*)
    1.49  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.50  (*val nxt = ("Specify_Problem", Specify_Problem *)
    1.51  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.52 -(*val nxt = ("Specify_Method",Specify_Method ("DiffAppl.thy","sqrt-equ-test"));*)
    1.53 +(*val nxt = ("Specify_Method",Specify_Method ("DiffAppl","sqrt-equ-test"));*)
    1.54  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.55 -(*val nxt = ("Apply_Method",Apply_Method ("DiffAppl.thy","sqrt-equ-test"));*)
    1.56 +(*val nxt = ("Apply_Method",Apply_Method ("DiffAppl","sqrt-equ-test"));*)
    1.57  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.58  val nxt = ("Free_Solve",Free_Solve);
    1.59  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.60 @@ -488,9 +488,9 @@
    1.61  val ((p,p_),_,f,nxt,_,pt)=
    1.62  me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [16] pt;
    1.63  (* 5.4.00.: ---
    1.64 -get_form ("Check_Postcond",Check_Postcond ("Test.thy","solve-root-equation")) (p,Met) pt;
    1.65 +get_form ("Check_Postcond",Check_Postcond ("Test","solve-root-equation")) (p,Met) pt;
    1.66  val (p,_,f,nxt,_,pt)=
    1.67 -me ("Check_Postcond",Check_Postcond ("Test.thy","solve-root-equation")) (p,Met) [17] pt;
    1.68 +me ("Check_Postcond",Check_Postcond ("Test","solve-root-equation")) (p,Met) [17] pt;
    1.69  --- *) 
    1.70  writeln (pr_ptree pr_short pt);
    1.71  writeln("result: "^(get_obj g_result pt [])^"\n==================================================================="*;
    1.72 @@ -504,7 +504,7 @@
    1.73  	   "solveFor x","errorBound (eps=0)",
    1.74  	   "solutions L"];
    1.75  val (dI',pI',mI') =
    1.76 -  ("Test.thy",["sqroot-test","univariate","equation","test"],
    1.77 +  ("Test",["sqroot-test","univariate","equation","test"],
    1.78     ["Test","sqrt-equ-test"]);
    1.79  "--- s1 ---";
    1.80  (*val p = e_pos'; val c = []; 
    1.81 @@ -529,7 +529,7 @@
    1.82  val nxt = ("Add_Find",Add_Find "solutions L");
    1.83  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.84  "--- s6 ---";
    1.85 -val nxt = ("Specify_Theory",Specify_Theory "Test.thy");
    1.86 +val nxt = ("Specify_Theory",Specify_Theory "Test");
    1.87  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.88  "--- s7 ---";
    1.89  val nxt = ("Specify_Problem",