313 "max_relation (A=#2*a*b - a^^^#2)", *) |
313 "max_relation (A=#2*a*b - a^^^#2)", *) |
314 "additionalRels [A=#2*a*b - a^^^#2,(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]", |
314 "additionalRels [A=#2*a*b - a^^^#2,(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]", |
315 "additionalRels [A=#2*a*b - a^^^#2,(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]", |
315 "additionalRels [A=#2*a*b - a^^^#2,(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]", |
316 "additionalRels [A=#2*a*b - a^^^#2,a=#2*R*sin alpha, b=#2*R*cos alpha]"]; |
316 "additionalRels [A=#2*a*b - a^^^#2,a=#2*R*sin alpha, b=#2*R*cos alpha]"]; |
317 val (dI',pI',mI')= |
317 val (dI',pI',mI')= |
318 ("DiffAppl.thy",["Script.thy","maximum_of","function"],e_metID); |
318 ("DiffAppl",["Script","maximum_of","function"],e_metID); |
319 val c = []:cid; |
319 val c = []:cid; |
320 |
320 |
321 (* |
321 (* |
322 val pbl = {given=["fixedValues [R=(R::real)]","boundVariable alpha", |
322 val pbl = {given=["fixedValues [R=(R::real)]","boundVariable alpha", |
323 "domain {x::real. #0 <= x & x <= pi//#2}", |
323 "domain {x::real. #0 <= x & x <= pi//#2}", |
414 "max_relation (A=#2*a*b - a^^^#2)", |
414 "max_relation (A=#2*a*b - a^^^#2)", |
415 "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]", |
415 "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]", |
416 "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]", |
416 "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]", |
417 "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"]; |
417 "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"]; |
418 val (dI',pI',mI')= |
418 val (dI',pI',mI')= |
419 ("DiffAppl.thy",["DiffAppl.thy","test_maximum"],e_metID); |
419 ("DiffAppl",["DiffAppl","test_maximum"],e_metID); |
420 val p = e_pos'; val c = []; |
420 val p = e_pos'; val c = []; |
421 |
421 |
422 val (mI,m) = ("Init_Proof",Init_Proof (cts, (dI',pI',mI'))); |
422 val (mI,m) = ("Init_Proof",Init_Proof (cts, (dI',pI',mI'))); |
423 val (pst as (sc,pt,cl):pstate) = (EmptyScr, e_ptree, []); |
423 val (pst as (sc,pt,cl):pstate) = (EmptyScr, e_ptree, []); |
424 val (p,_,f,nxt,_,(_,pt,_)) = do_ (mI,m) p c pst; |
424 val (p,_,f,nxt,_,(_,pt,_)) = do_ (mI,m) p c pst; |