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") *)