wneuper/isa: comparison test/Tools/isac/Knowledge/rlang.sml

equal deleted inserted replaced

-:24609758d219
+:028442673981
 "Schalk I s.86 Bsp 5 (3*x - 1 - (5*x - (2 - 4*x)) = -11)";
 "Schalk I s.86 Bsp 5 (3*x - 1 - (5*x - (2 - 4*x)) = -11)";
 (*EP*)
 val fmz = ["equality (3*x - 1 - (5*x - (2 - 4*x)) = -11)",
 	   "solveFor x","solutions L"];
-val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
+val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
 (*val p = e_pos';
 val c = [];
 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 "Schalk I s.86 Bsp 19 (x - 5)*(10 - x) = (3 - x)*(2 + x) + 2*(x + 20)";
 "Schalk I s.86 Bsp 19 (x - 5)*(10 - x) = (3 - x)*(2 + x) + 2*(x + 20)";
 (*EP*)
 val fmz = ["equality ((x - 5)*(10 - x) = (3 - x)*(2 + x) + 2*(x + 20))",
 	   "solveFor x","solutions L"];
-val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
+val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
 (*val p = e_pos';
 val c = [];
 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 "Schalk I s.86 Bsp 19 ((2*x+5)^^^2+(3*x+4)^^^2=(13*x+2)*(x+1)+2*(15+14*x))";
 "Schalk I s.86 Bsp 19 ((2*x+5)^^^2+(3*x+4)^^^2=(13*x+2)*(x+1)+2*(15+14*x))";
 (*EP*)
 val fmz = ["equality ((2*x+5)^^^2+(3*x+4)^^^2=(13*x+2)*(x+1)+2*(15+14*x))",
 	   "solveFor x","solutions L"];
-val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
+val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
 (*val p = e_pos';
 val c = [];
 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 "Schalk I s.86 Bsp 25 ((2*x+1)^^^3+(x+1)^^^3=(2*x+1)^^^2*2*x+(x+2)^^^3+x^^^2)";
 "Schalk I s.86 Bsp 25 ((2*x+1)^^^3+(x+1)^^^3=(2*x+1)^^^2*2*x+(x+2)^^^3+x^^^2)";
 (*EP*)
 val fmz = ["equality ((2*x+1)^^^3+(x+1)^^^3=(2*x+1)^^^2*2*x+(x+2)^^^3+x^^^2)",
 	   "solveFor x","solutions L"];
-val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
+val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
 (*val p = e_pos';
 val c = [];
 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 "Schalk I s.86 Bsp 28b ((3*x+5)/18 - x/2 = -((3*x - 2)/9))";
 "Schalk I s.86 Bsp 28b ((3*x+5)/18 - x/2 = -((3*x - 2)/9))";
 (*ER-2*)
 val fmz = ["equality ((3*x+5)/18 - x/2 = -((3*x - 2)/9))",
 	   "solveFor x","solutions L"];
-val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
+val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
 (*val p = e_pos'; val c = [];
 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 "Schalk I s.87 Bsp 36b ((17*x - 51)/9 - (-(13*x - 3)/6) + 11 -(9*x- 7)/4 = 0)";
 "Schalk I s.87 Bsp 36b ((17*x - 51)/9 - (-(13*x - 3)/6) + 11 -(9*x- 7)/4 = 0)";
 (*ER-1*)
 val fmz = ["equality ((17*x - 51)/9 - (-(13*x - 3)/6) + 11 - (9*x - 7)/4 = 0)",
 	   "solveFor x","solutions L"];
-val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
+val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
 (*val p = e_pos';
 val c = [];
 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 "Schalk I s.87 Bsp 38b (-(2/x) + 3/(2*x) - 4/(3*x) + 5/(4*x) + 6/(5*x) =65/8)";
 "Schalk I s.87 Bsp 38b (-(2/x) + 3/(2*x) - 4/(3*x) + 5/(4*x) + 6/(5*x) =65/8)";
 (*ER-3*)
 val fmz = ["equality (-2/x + 3/(2*x) - 4/(3*x) + 5/(4*x) + 6/(5*x) = 65/8)",
 	   "solveFor x","solutions L"];
-val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
+val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
 (*val p = e_pos';
 val c = [];
 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 "Schalk I s.87 Bsp 40b ((x+3)/(2*x - 4)=3)";
 "Schalk I s.87 Bsp 40b ((x+3)/(2*x - 4)=3)";
 (*ER-4*)
 val fmz = ["equality ((x+3)/(2*x - 4)=3)",
 	   "solveFor x","solutions L"];
-val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
+val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
 (*val p = e_pos';
 val c = [];
 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 "Schalk I s.87 Bsp 44a ((1/2+(5*x)/2)^^^2 -((13*x)/2- 5/2)^^^2 -(6*x)^^^2+29)";
 "Schalk I s.87 Bsp 44a ((1/2+(5*x)/2)^^^2 -((13*x)/2- 5/2)^^^2 -(6*x)^^^2+29)";
 (*ER-5*)
 val fmz = ["equality ((1/2 + (5*x)/2)^^^2 - ((13*x)/2 - 5/2)^^^2 = -1*(6*x)^^^2 + 29)",
 	   "solveFor x","solutions L"];
-val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
+val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
 (*val p = e_pos';
 val c = [];
 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 "Schalk I s.87 Bsp 52a ((5*x)/(x - 2) - x/(x+2)=4)";
 "Schalk I s.87 Bsp 52a ((5*x)/(x - 2) - x/(x+2)=4)";
 (*ER-6*)
 val fmz = ["equality ((5*x)/(x - 2) - x/(x+2)=4)",
 	   "solveFor x","solutions L"];
-val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
+val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 "Schalk I s.87 Bsp 55b (x/(x^^^2 - 6*x+9) - 1/(x^^^2 - 3*x) =1/x)";
 "Schalk I s.87 Bsp 55b (x/(x^^^2 - 6*x+9) - 1/(x^^^2 - 3*x) =1/x)";
 (*ER-7*)
 val fmz = ["equality (x/(x^^^2 - 6*x+9) - 1/(x^^^2 - 3*x) =1/x)",
 	   "solveFor x","solutions L"];
-val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
+val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 (*val nxt = ("Model_Problem",Model_Problem["rational","univariate","equation"*)
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; 040209 MGs norm_Rational*)
-(* val nxt = Subproblem ("PolyEq.thy",["polynomial","univariate","equation"])*)
+(* val nxt = Subproblem ("PolyEq",["polynomial","univariate","equation"])*)
 if f= Form' (FormKF (~1, EdUndef, 0, Nundef, "-6 * x + 5 * x ^^^ 2 = 0"))then()
 else raise error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b";
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 (*nxt=Model_Problem["bdv_only","degree_2","polynomial","univariate","equation*)
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 "Schalk I s.88 Bsp 64c (((x - 1)/(x+1)+1)/((x - 1)/(x+1) - (x+1)/(x - 1))=2)";
 "Schalk I s.88 Bsp 64c (((x - 1)/(x+1)+1)/((x - 1)/(x+1) - (x+1)/(x - 1))=2)";
 (*ER-8*)
 val fmz = ["equality (((x - 1)/(x+1)+1)/((x - 1)/(x+1) - (x+1)/(x - 1))=2)",
 	   "solveFor x","solutions L"];
-val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
+val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
 (*val p = e_pos'; val c = [];
 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 "Schalk I s.88 Bsp 79a (2) (m1*v1+m2*v2=0)";
 "Schalk I s.88 Bsp 79a (2) (m1*v1+m2*v2=0)";
 (*ER-10*)
 val fmz = ["equality (m1*v1+m2*v2=0)",
 	   "solveFor m1","solutions L"];
-val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
+val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
 (*val p = e_pos'; val c = [];
 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 "Schalk I s.89 Bsp 90a (1) (f=((w+u)/(w+v))*v0)";
 "Schalk I s.89 Bsp 90a (1) (f=((w+u)/(w+v))*v0)";
 (*ER-11*)
 val fmz = ["equality (f=((w+u)/(w+v))*v0)",
 	   "solveFor v","solutions L"];
-val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
+val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
 (*val p = e_pos'; val c = [];
 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 (*val nxt = Specify_Method ["RatEq","solve_rat_equation"])      *)
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
-(*nxt = Subproblem ("RatEq.thy",["univariate","equation"]))      *)
+(*nxt = Subproblem ("RatEq",["univariate","equation"]))      *)
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 (*val nxt =Model_Problem ["normalize","polynomial","univariate","equation"])*)
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 (*val nxt = ("Apply_Method",Apply_Method ["PolyEq","normalize_poly"])*)
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
-(*val nxt =Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))*)
+(*val nxt =Subproblem ("PolyEq",["polynomial","univariate","equation"]))*)
 if f = Form'
 (FormKF
 (~1,
 EdUndef,
 0,
 "Schalk I s.89 Bsp 90a (2) (f=((w+u)/(w+v))*v0)";
 "Schalk I s.89 Bsp 90a (2) (f=((w+u)/(w+v))*v0)";
 (*ER-12*)
 val fmz = ["equality (f=((w+u)/(w+v))*v0)",
 	   "solveFor w","solutions L"];
-val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
+val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
 (*val p = e_pos';val c = [];
 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 "Schalk I s.89 Bsp 98a (1) (1/R=1/R1+1/R2)";
 "Schalk I s.89 Bsp 98a (1) (1/R=1/R1+1/R2)";
 (*ER-9*)
 val fmz = ["equality (1/R=1/R1+1/R2)",
 	   "solveFor R1","solutions L"];
-val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
+val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
 (*val p = e_pos'; val c = [];
 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 "Schalk I s.89 Bsp 104a (1) (y^^^2=2*p*x)";
 "Schalk I s.89 Bsp 104a (1) (y^^^2=2*p*x)";
 (*ER-13 + EO-11 ?!?*)
 val fmz = ["equality (y^^^2=2*p*x)",
 	   "solveFor p","solutions L"];
-val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
+val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
 (*val p = e_pos'; val c = [];
 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 "Schalk I s.89 Bsp 104a (2) (y^^^2=2*p*x)";
 "Schalk I s.89 Bsp 104a (2) (y^^^2=2*p*x)";
 (*EO ??*)
 val fmz = ["equality (y^^^2=2*p*x)",
 	   "solveFor y","solutions L"];
-val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
+val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
 (*val p = e_pos';
 val c = [];
 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 "Schalk I s.90 Bsp 118a (1) (b^^^2*x^^^2 + a^^^2*y^^^2 = a^^^2*b^^^2)";
 "Schalk I s.90 Bsp 118a (1) (b^^^2*x^^^2 + a^^^2*y^^^2 = a^^^2*b^^^2)";
 (*EO-8*)
 val fmz = ["equality (b^^^2*x^^^2 + a^^^2*y^^^2 = a^^^2*b^^^2)",
 	   "solveFor x","solutions L"];
-val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
+val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
 (*val p = e_pos';
 val c = [];
 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 "Schalk I s.102 Bsp 268(1) (A = (1/2)*(x1*(y2-y3)+x2*(y3 - y1)+x3*(y1 - y2)))";
 "Schalk I s.102 Bsp 268(1) (A = (1/2)*(x1*(y2-y3)+x2*(y3 - y1)+x3*(y1 - y2)))";
 (*ER-14*)
 val fmz = ["equality (A = (1/2)*(x1*(y2 - y3)+x2*(y3 - y1)+x3*(y1 - y2)))",
 	   "solveFor x2","solutions L"];
-val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
+val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
 (*val p = e_pos';
 val c = [];
 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 "Schalk II s.56 Bsp 67b (4*sqrt(4*x+1)=3*sqrt(7*x+2))";
 "Schalk II s.56 Bsp 67b (4*sqrt(4*x+1)=3*sqrt(7*x+2))";
 (*EO*)
 val fmz = ["equality (4*sqrt(4*x+1)=3*sqrt(7*x+2))",
 	   "solveFor x","solutions L"];
-val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
+val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
 (*val p = e_pos';
 val c = [];
 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 "Schalk II s.56 Bsp 68a (5*sqrt(x) - 1 = 7*sqrt(x) - 5)";
 "Schalk II s.56 Bsp 68a (5*sqrt(x) - 1 = 7*sqrt(x) - 5)";
 "Schalk II s.56 Bsp 68a (5*sqrt(x) - 1 = 7*sqrt(x) - 5)";
 val fmz = ["equality (5*sqrt(x) - 1 = 7*sqrt(x) - 5)",
 	   "solveFor x","solutions L"];
-val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
+val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
 (*val p = e_pos';
 val c = [];
 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 "Schalk II s.56 Bsp 73b (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))";
 "Schalk II s.56 Bsp 73b (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))";
 (*EO-2*)
 val fmz = ["equality (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))",
 	   "solveFor x","solutions L"];
-val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
+val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 (*"13 + 13 * x + -2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x"
--> Subproblem ("RootEq.thy", ["univariate", ...])*)
+-> Subproblem ("RootEq", ["univariate", ...])*)
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 (*"144 + 288 * x + 144 * x ^^^ 2 = 144 + x ^^^ 2 + 288 * x + 143 * x ^^^ 2"
--> Subproblem ("RootEq.thy", ["univariate", ...])*)
+-> Subproblem ("RootEq", ["univariate", ...])*)
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 "Schalk II s.56 Bsp 74a (sqrt(4*x+1) - sqrt(x+3) = sqrt(x - 2))";
 "Schalk II s.56 Bsp 74a (sqrt(4*x+1) - sqrt(x+3) = sqrt(x - 2))";
 (*EO-3*)
 val fmz = ["equality (sqrt(4*x+1) - sqrt(x+3) = sqrt(x - 2))",
 	   "solveFor x","solutions L"];
-val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
+val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 (*4 + 5 * x + -2 * sqrt (3 + 13 * x + 4 * x ^^^ 2) = -2 + x"
--> Subproblem ("RootEq.thy", ["univariate", ...])*)
+-> Subproblem ("RootEq", ["univariate", ...])*)
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 (*"12 + 52 * x + 16 * x ^^^ 2 = 36 + x ^^^ 2 + 48 * x + 15 * x ^^^ 2"
--> Subproblem ("RootEq.thy", ["univariate", ...])*)
+-> Subproblem ("RootEq", ["univariate", ...])*)
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-24 + 4 * x = 0")) then ()
 else raise error "rlang.sml: diff.behav. in Schalk II s.56 Bsp 74a";
-(*-> ubproblem ("PolyEq.thy", ["degree_1", ...]*)
+(*-> ubproblem ("PolyEq", ["degree_1", ...]*)
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 "Schalk II s.56 Bsp 77b (sqrt(x+12)+sqrt(x - 3) = sqrt(x + 32) - sqrt(5+x))";
 "Schalk II s.56 Bsp 77b (sqrt(x+12)+sqrt(x - 3) = sqrt(x + 32) - sqrt(5+x))";
 (*EO-4*)
 val fmz = ["equality (sqrt(x+12)+sqrt(x - 3) = sqrt(x + 32) - sqrt(5+x))",
 	   "solveFor x","solutions L"];
-val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
+val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 (* val nxt = ("Model_Problem",Model_Problem ["sq","root'","univariate","equation"]) *)
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 "Schalk II s.66 Bsp 4 ((6*x - 9)*(5*x+7) - (4*x+7)*(3*x - 6) = 429)";
 "Schalk II s.66 Bsp 4 ((6*x - 9)*(5*x+7) - (4*x+7)*(3*x - 6) = 429)";
 (*EP*)
 val fmz = ["equality ((6*x - 9)*(5*x+7) - (4*x+7)*(3*x - 6) = 429)",
 	   "solveFor x","solutions L"];
-val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
+val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
 (*val p = e_pos';
 val c = [];
 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 (*-----------------  Schalk II s.66 Bsp 8a ------------------------*)
 "Schalk II s.66 Bsp 8a ((x - 4)/(x+4) = (1 - x)/(1+x))";
 (*ER-15*)
 val fmz = ["equality ((x - 4)/(x+4) = (1 - x)/(1+x))",
 	   "solveFor x","solutions L"];
-val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
+val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; f2str f;
 (*"(-4 + x) * (1 + x) = (1 + -1 * x) * (4 + x)"
--> Subproblem ("RatEq.thy", ["univariate", ...])*)
+-> Subproblem ("RatEq", ["univariate", ...])*)
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-8 + 2 * x ^^^ 2 = 0")) then ()
 else raise error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 8a";
-(*-> Subproblem ("PolyEq.thy", ["polynomial", ...])*)
+(*-> Subproblem ("PolyEq", ["polynomial", ...])*)
 (*
 val Form' (FormKF (~1, EdUndef, 0, Nundef, str)) = f;
 *)
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 "Schalk II s.66 Bsp 10b (1/(x^^^2 - 9)+(2*x+3)/(x+3)=(3*x+4)/(x - 3))";
 "Schalk II s.66 Bsp 10b (1/(x^^^2 - 9)+(2*x+3)/(x+3)=(3*x+4)/(x - 3))";
 "Schalk II s.66 Bsp 10b (1/(x^^^2 - 9)+(2*x+3)/(x+3)=(3*x+4)/(x - 3))";
 val fmz = ["equality (1/(x^^^2 - 9)+(2*x+3)/(x+3)=(3*x+4)/(x - 3))",
 	   "solveFor x","solutions L"];
-val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
+val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
 (*val p = e_pos';
 val c = [];
 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 "Schalk II s.66 Bsp 20a (sqrt(29 - sqrt (x^^^2 - 9))=5)";
 "Schalk II s.66 Bsp 20a (sqrt(29 - sqrt (x^^^2 - 9))=5)";
 "Schalk II s.66 Bsp 20a (sqrt(29 - sqrt (x^^^2 - 9))=5)";
 val fmz = ["equality (sqrt(29 - sqrt(x^^^2 - 9))=5)",
 	   "solveFor x","solutions L"];
-val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
+val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
 (*val p = e_pos';
 val c = [];
 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 	### or2list False
 ([6, 6, 3, 1], Res) "False"
 *)
 val fmz = ["equality (2*sqrt(261 - x) - sqrt(2+2*x)=sqrt(2)*sqrt(5 - 3*x))",
 	   "solveFor x","solutions L"];
-val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
+val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 "Schalk II s.66 Bsp 28a (A=(c/d)*sqrt(4*a^^^2 - c^^^2))";
 "Schalk II s.66 Bsp 28a (A=(c/d)*sqrt(4*a^^^2 - c^^^2))";
 "Schalk II s.66 Bsp 28a (A=(c/d)*sqrt(4*a^^^2 - c^^^2))";
 val fmz = ["equality (A=(c/d)*sqrt(4*a^^^2 - c^^^2))",
 	   "solveFor a","solutions L"];
-val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
+val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
 (*val p = e_pos';
 val c = [];
 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 (*-----------------  Schalk II s.68 Bsp 52b ------------------------*)
 "Schalk II s.68 Bsp 52b (1/(x - a+b)=1/x - 1/a + 1/b)";
 val fmz = ["equality (1/(x - a+b)=1/x - 1/a + 1/b)",
 	   "solveFor x","solutions L"];
-val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
+val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 (* val nxt = ("Model_Problem",Model_Problem ["rational","univariate","equation"])*)
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
-(*val nxt = ("Specify_Theory",Specify_Theory "RatEq.thy")*)
+(*val nxt = ("Specify_Theory",Specify_Theory "RatEq")*)
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 (*val p = ([3],Res)
 val f="1 * (a * (b * x)) = (a * b + (a * x + -1 * (b * x))) * (b + (x + -1 * a)
-val nxt = Subproblem ("RatEq.thy",["univariate","equation"]))*)
+val nxt = Subproblem ("RatEq",["univariate","equation"]))*)
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
-(*val nxt = ("Specify_Theory",Specify_Theory "PolyEq.thy")*)
+(*val nxt = ("Specify_Theory",Specify_Theory "PolyEq")*)
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 (* nxt = Specify_Problem ["normalize","polynomial","univariate","equation"])*)
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; at introducing of MGs norm_Rational*)
 (*val p = ([4,5],Res)  val f ="b * a ^^^ 2 + -1 * a * b ^^^ 2 + (a ^^^ 2 + b ^^^ 2 + -2 * a * b) * x +\n(b + -1 * a) * x ^^^ 2 =\n0"))
-val nxt = Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))*)
+val nxt = Subproblem ("PolyEq",["polynomial","univariate","equation"]))*)
 if f = Form'
 (FormKF
 (~1,
 EdUndef,
 0,
 "b * a ^^^ 2 + -1 * a * b ^^^ 2 + (a ^^^ 2 + b ^^^ 2 + -2 * a * b) * x +\n(b + -1 * a) * x ^^^ 2 =\n0")) then ()
 else raise error "rlang.sml: diff.behav. in chalk I s.87 Bsp 38b";
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
-(*val nxt = ("Specify_Theory",Specify_Theory "PolyEq.thy")*)
+(*val nxt = ("Specify_Theory",Specify_Theory "PolyEq")*)
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 (*Specify_Problem["abcFormula","degree_2","polynomial","univariate","equation*)
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 else raise error "rlang.sml: diff.behav. in rational-a-b";
 (*-----------------  Schalk II s.68 Bsp 56a ------------------------*)
 "Schalk II s.68 Bsp 56a ((a+b*x)/(a-b*x) - (a - b*x)/(a+b*x)= (4*a*b)/(a^^^2 - b^^^2))";
 val fmz = ["equality ((a+b*x)/(a-b*x) - (a - b*x)/(a+b*x)= (4*a*b)/(a^^^2 - b^^^2))","solveFor x","solutions L"];
-val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
+val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 (* val nxt = ("Model_Problem",Model_Problem ["rational","univariate","equation"]) *)
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 (*-----------------  Schalk II s.68 Bsp 61b ------------------------*)
 "Schalk II s.68 Bsp 61b (sqrt(x+a)+sqrt(b - x)=sqrt(a+b))";
 val fmz = ["equality (sqrt(x+a)+sqrt(b - x)=sqrt(a+b))",
 	   "solveFor x","solutions L"];
-val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
+val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 (* val nxt = ("Model_Problem",Model_Problem ["sq","root'","univariate","equation"])*)
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 (*-----------------  Schalk II s.68 Bsp 62b ------------------------*)
 "Schalk II s.68 Bsp 62b (sqrt((x+a)^^^2+(x - 2*b)^^^2)=a+2*b)";
 val fmz = ["equality (sqrt((x+a)^^^2+(x - 2*b)^^^2)=a+2*b)",
 	   "solveFor x","solutions L"];
-val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
+val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 (*val nxt = ("Model_Problem",Model_Problem ["sq","root'","univariate","equation"]) *)
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 "------ WN.TEST---------------------------------";
 "------ WN.TEST---------------------------------";
 (*EO-7*)
 val fmz = ["equality ((2*x+1)*x^^^2 = 0)",
 	   "solveFor x","solutions L"];
-val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
+val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 "-------------------- WN.15.5.03: Pythagoras -------------------------------";
 "-------------------- WN.15.5.03: Pythagoras -------------------------------";
 (*EO-9*)
 val fmz = ["equality ((a/2)^^^2 + (b/2)^^^2 = r^^^2)",
 	   "solveFor a","solutions L"];
-val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
+val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 (*   Model_Problem ["normalize","polynomial","univariate","equation"])*)
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 (*val nxt = ("Apply_Method",Apply_Method ["PolyEq","normalize_poly"])*)
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
-(*val nxt = Subproblem ("PolyEq.thy",["polynomial","univariate","equation"])*)
+(*val nxt = Subproblem ("PolyEq",["polynomial","univariate","equation"])*)
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 (*val nxt =Model_Problem ["sq_only","degree_2","polynomial","univariate","equation"])*)
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 "-------------------- WN.15.5.03: equation within the maximum example ------";
 "-------------------- WN.15.5.03: equation within the maximum example ------";
 (*EO-10*)
 val fmz = ["equality (2*sqrt(r^^^2 - (u/2)^^^2) - u^^^2/(2*sqrt(r^^^2 - (u/2)^^^2))= 0)",
 	   "solveFor u","solutions L"];
-val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
+val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 (*   Model_Problem ["normalize","root'","univariate","equation"])*)
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 (*val nxt = Apply_Method ["RootEq","norm_sq_root_equation"])     *)
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
-(*val nxt = Subproblem ("RootEq.thy",["univariate","equation"]))*)
+(*val nxt = Subproblem ("RootEq",["univariate","equation"]))*)
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 (*val nxt = Model_Problem ["sq","root'","univariate","equation"]) *)
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 (*val nxt = Apply_Method ["RootEq","solve_sq_root_equation"])     *)
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
-(*val nxt = Subproblem ("RootEq.thy",["univariate","equation"]))*)
+(*val nxt = Subproblem ("RootEq",["univariate","equation"]))*)
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 (*val nxt = Model_Problem ["rational","univariate","equation"]) *)
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 (*val nxt = Apply_Method ["RootEq","solve_rat_equation"])     *)
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
-(*val nxt = Subproblem ("RootEq.thy",["univariate","equation"]))*)
+(*val nxt = Subproblem ("RootEq",["univariate","equation"]))*)
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 (*val nxt = Model_Problem ["normalize","polynomial","univariate","equation"]) *)
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 (*val nxt = Apply_Method ["PolyEq","normalize_poly"])     *)
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
-(*val nxt = Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))*)
+(*val nxt = Subproblem ("PolyEq",["polynomial","univariate","equation"]))*)
 if f = Form'
 (FormKF
 (~1,
 EdUndef,
 0,

branch	isac-update-Isa09-2
changeset 37991	028442673981
parent 37986	7b1d2366c191
child 38031	460c24a6a6ba