478 "--- 9 ---"; |
478 "--- 9 ---"; |
479 get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt; |
479 get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt; |
480 val (p,_,f,nxt,_,pt)= |
480 val (p,_,f,nxt,_,pt)= |
481 me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [14] pt; |
481 me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [14] pt; |
482 "--- 10 ---."; |
482 "--- 10 ---."; |
483 get_form ("Rewrite_Set_Inst",Rewrite_Set_Inst (["(bdv,x)"],"isolate_bdv")) p pt; |
483 get_form ("Rewrite_Set_Inst",Rewrite_Set_Inst (["(''bdv'',x)"],"isolate_bdv")) p pt; |
484 val (p,_,f,nxt,_,pt)= |
484 val (p,_,f,nxt,_,pt)= |
485 me ("Rewrite_Set",Rewrite_Set_Inst (["(bdv,x)"],"isolate_bdv")) p [15] pt; |
485 me ("Rewrite_Set",Rewrite_Set_Inst (["(''bdv'',x)"],"isolate_bdv")) p [15] pt; |
486 "--- 11 ---"; |
486 "--- 11 ---"; |
487 get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt; |
487 get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt; |
488 val ((p,p_),_,f,nxt,_,pt)= |
488 val ((p,p_),_,f,nxt,_,pt)= |
489 me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [16] pt; |
489 me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [16] pt; |
490 (* 5.4.00.: --- |
490 (* 5.4.00.: --- |
579 \Try (Rewrite_Set Test_simplify False) @@\ |
579 \Try (Rewrite_Set Test_simplify False) @@\ |
580 \Try (Rewrite_Set rearrange_assoc False) @@\ |
580 \Try (Rewrite_Set rearrange_assoc False) @@\ |
581 \Try (Rewrite_Set Test_simplify False)) @@\ |
581 \Try (Rewrite_Set Test_simplify False)) @@\ |
582 \Try (Rewrite_Set norm_equation False) @@\ |
582 \Try (Rewrite_Set norm_equation False) @@\ |
583 \Try (Rewrite_Set Test_simplify False) @@\ |
583 \Try (Rewrite_Set Test_simplify False) @@\ |
584 \Rewrite_Set_Inst [(bdv, v_v)] isolate_bdv False @@\ |
584 \Rewrite_Set_Inst [(''bdv'', v_v)] isolate_bdv False @@\ |
585 \Try (Rewrite_Set Test_simplify False))\ |
585 \Try (Rewrite_Set Test_simplify False))\ |
586 \e_)"; |
586 \e_)"; |
587 |
587 |
588 -------------------------*) |
588 -------------------------*) |
589 |
589 |
617 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
617 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
618 "--- 11<> ---."; |
618 "--- 11<> ---."; |
619 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify"); |
619 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify"); |
620 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
620 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
621 "--- 12<> ---"; |
621 "--- 12<> ---"; |
622 val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst (["(bdv,x)"],"isolate_bdv")); |
622 val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst (["(''bdv'',x)"],"isolate_bdv")); |
623 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
623 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
624 "--- 13<> ---"; |
624 "--- 13<> ---"; |
625 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify"); |
625 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify"); |
626 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
626 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
627 "--- 1<> ---"; |
627 "--- 1<> ---"; |