src/Tools/isac/Knowledge/DiffApp-scrpbl.sml
changeset 59406 509d70b507e5
parent 59279 255c853ea2f0
child 59416 229e5c9cf78b
     1.1 --- a/src/Tools/isac/Knowledge/DiffApp-scrpbl.sml	Thu Mar 15 10:17:44 2018 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/DiffApp-scrpbl.sml	Thu Mar 15 12:42:04 2018 +0100
     1.3 @@ -315,7 +315,7 @@
     1.4   "additionalRels [A=#2*a*b - a^^^#2,(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]",
     1.5   "additionalRels [A=#2*a*b - a^^^#2,a=#2*R*sin alpha, b=#2*R*cos alpha]"];
     1.6  val (dI',pI',mI')=
     1.7 -  ("DiffAppl",["Script","maximum_of","function"],e_metID);
     1.8 +  ("DiffAppl",["Script","maximum_of","function"],Celem.e_metID);
     1.9  val c = []:cid;
    1.10  
    1.11  (*
    1.12 @@ -416,14 +416,14 @@
    1.13  	   "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]",
    1.14  	   "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"];
    1.15  val (dI',pI',mI')=
    1.16 -  ("DiffAppl",["DiffAppl","test_maximum"],e_metID);
    1.17 +  ("DiffAppl",["DiffAppl","test_maximum"],Celem.e_metID);
    1.18  val p = e_pos'; val c = []; 
    1.19  
    1.20  val (mI,m) = ("Init_Proof",Init_Proof (cts, (dI',pI',mI')));
    1.21 -val (pst as (sc,pt,cl):pstate) = (EmptyScr, e_ctree, []);
    1.22 +val (pst as (sc,pt,cl):pstate) = (Celem.EmptyScr, e_ctree, []);
    1.23  val (p,_,f,nxt,_,(_,pt,_)) = do_ (mI,m) p c pst;
    1.24  (*val nxt = ("Add_Given",Add_Given "fixedValues [R = R]")*)
    1.25  
    1.26  val (p,_,Form' (PpcKF (_,_,ppc)),nxt,_,(_,pt,_)) = 
    1.27 -  do_ nxt p c (EmptyScr,pt,[]);
    1.28 +  do_ nxt p c (Celem.EmptyScr,pt,[]);
    1.29  (*val nxt = ("Add_Given",Add_Given "boundVariable a") *)