1.1 --- a/src/Tools/isac/Knowledge/DiffApp-scrpbl.sml	Sat May 02 10:57:04 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/DiffApp-scrpbl.sml	Sat May 02 11:36:13 2020 +0200
     1.3 @@ -332,8 +332,7 @@
     1.4  	   "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"]
     1.5  	   }: string ppc;
     1.6  *)
     1.7 -val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = 
     1.8 -  specify (Init_Proof (cts,(dI',pI',mI'))) e_pos' [] EmptyPtree;
     1.9 +val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = Test_Code.CalcTreeTEST [(cts, (dI',pI',mI'))];
    1.10  
    1.11  val ct = "fixedValues [R=(R::real)]";
    1.12  (*l(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify(Add_Given ct) p c pt*)
    1.13 @@ -375,16 +374,14 @@
    1.14  *)
    1.15  *)
    1.16  (* --- tricky case (termlist interleaving variants):
    1.17 -> val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = 
    1.18 -  specify (Init_Proof (cts,(dI,pI,mI))) [] [] EmptyPtree;
    1.19 +> val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = Test_Code.CalcTreeTEST [(cts, (dI',pI',mI'))];
    1.20  
    1.21  > val ct = "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2, b=#2*R*cos alpha]";
    1.22  > val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
    1.23  *)
    1.24  
    1.25  (* --- incomplete input ---
    1.26 -> val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = 
    1.27 -  specify (Init_Proof (cts,(dI,pI,mI))) [] [] EmptyPtree;
    1.28 +> val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = Test_Code.CalcTreeTEST [(cts, (dI',pI',mI'))];
    1.29  
    1.30  > val ct = "[R=(R::real)]";
    1.31  > val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
    1.32 @@ -419,6 +416,7 @@
    1.33    ("DiffAppl",["DiffAppl","test_maximum"],Method.id_empty);
    1.34  val p = e_pos'; val c = []; 
    1.35  
    1.36 +(*/------- Init_Proof replaced by Test_Code.CalcTreeTEST ------------------------------------\* )
    1.37  val (mI,m) = ("Init_Proof",Init_Proof (cts, (dI',pI',mI')));
    1.38  val (pst as (sc,pt,cl):pstate) = (Rule.Empty_Prog, e_ctree, []);
    1.39  val (p,_,f,nxt,_,(_,pt,_)) = do_ (mI,m) p c pst;
    1.40 @@ -427,3 +425,4 @@
    1.41  val (p,_,Form' (PpcKF (_,_,ppc)),nxt,_,(_,pt,_)) = 
    1.42    do_ nxt p c (Rule.Empty_Prog,pt,[]);
    1.43  (*val nxt = ("Add_Given",Add_Given "boundVariable a") *)
    1.44 +( *\------- Init_Proof replaced by Test_Code.CalcTreeTEST ------------------------------------/*)