1.1 --- a/src/Tools/isac/Knowledge/DiffApp-scrpbl.sml	Wed Sep 08 16:45:27 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/DiffApp-scrpbl.sml	Wed Sep 08 16:47:22 2010 +0200
     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.thy",["Script.thy","maximum_of","function"],e_metID);
     1.8 +  ("DiffAppl",["Script","maximum_of","function"],e_metID);
     1.9  val c = []:cid;
    1.10  
    1.11  (*
    1.12 @@ -416,7 +416,7 @@
    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.thy",["DiffAppl.thy","test_maximum"],e_metID);
    1.17 +  ("DiffAppl",["DiffAppl","test_maximum"],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')));