143 (*val it = SOME ["pbla2","pbla"] : pblID option*) |
143 (*val it = SOME ["pbla2","pbla"] : pblID option*) |
144 |
144 |
145 (*case 4: refined to children (without child)*) |
145 (*case 4: refined to children (without child)*) |
146 val opt = refine_ori ori4 ["pbla"]; |
146 val opt = refine_ori ori4 ["pbla"]; |
147 if opt = SOME ["pbla2y","pbla2","pbla"] then () |
147 if opt = SOME ["pbla2y","pbla2","pbla"] then () |
148 else raise error "new behaviour in refine.sml case 4"; |
148 else error "new behaviour in refine.sml case 4"; |
149 |
149 |
150 (*case 5: start refinement somewhere in ptyps*) |
150 (*case 5: start refinement somewhere in ptyps*) |
151 refine_ori ori4 ["pbla2","pbla"]; |
151 refine_ori ori4 ["pbla2","pbla"]; |
152 (*val it = SOME ["pbla2y","pbla2","pbla"] : pblID option*) |
152 (*val it = SOME ["pbla2y","pbla2","pbla"] : pblID option*) |
153 |
153 |
417 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
417 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
418 (*Check_Postcond ["normalize","univariate","equation","test"])*) |
418 (*Check_Postcond ["normalize","univariate","equation","test"])*) |
419 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
419 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
420 val Form' (FormKF (~1,EdUndef,_,Nundef,res)) = f; |
420 val Form' (FormKF (~1,EdUndef,_,Nundef,res)) = f; |
421 if (snd nxt)=End_Proof' andalso res="[x = 2]" then () |
421 if (snd nxt)=End_Proof' andalso res="[x = 2]" then () |
422 else raise error "new behaviour in test:refine.sml:miniscript with mini-subpb"; |
422 else error "new behaviour in test:refine.sml:miniscript with mini-subpb"; |
423 |
423 |
424 |
424 |
425 "----------- fun coll_guhs ---------------------------------------"; |
425 "----------- fun coll_guhs ---------------------------------------"; |
426 "----------- fun coll_guhs ---------------------------------------"; |
426 "----------- fun coll_guhs ---------------------------------------"; |
427 "----------- fun coll_guhs ---------------------------------------"; |
427 "----------- fun coll_guhs ---------------------------------------"; |