418 val (dI',pI',mI')= |
418 val (dI',pI',mI')= |
419 ("DiffAppl",["DiffAppl","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_ctree, []); |
424 val (p,_,f,nxt,_,(_,pt,_)) = do_ (mI,m) p c pst; |
424 val (p,_,f,nxt,_,(_,pt,_)) = do_ (mI,m) p c pst; |
425 (*val nxt = ("Add_Given",Add_Given "fixedValues [R = R]")*) |
425 (*val nxt = ("Add_Given",Add_Given "fixedValues [R = R]")*) |
426 |
426 |
427 val (p,_,Form' (PpcKF (_,_,ppc)),nxt,_,(_,pt,_)) = |
427 val (p,_,Form' (PpcKF (_,_,ppc)),nxt,_,(_,pt,_)) = |
428 do_ nxt p c (EmptyScr,pt,[]); |
428 do_ nxt p c (EmptyScr,pt,[]); |