neuper@41985: (* Title:  400-start-meth-subpbl.sml
neuper@41985:    Author: Walther Neuper 1105
neuper@41985:    (c) copyright due to lincense terms.
neuper@41985: *)
neuper@41985: 
neuper@41985: val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
neuper@41985: val (dI',pI',mI') =
neuper@41990:    ("Test", ["sqroot-test","univariate","equation","test"],
neuper@41990:     ["Test","squ-equ-test-subpbl1"]);
neuper@41985: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@41985: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41990: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41990: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41990: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41990: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41990: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41990: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41990: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41990: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41990: val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Subproblem"*)
neuper@41990: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41990: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41990: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41990: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41990: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41990: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41990: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41990: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41990: val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst isolate_bdv*);
neuper@41990: val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*);
neuper@41990: val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["linear","univariate", ...]) *);
neuper@41990: (*-----nxt = ("Empty_Tac", Empty_Tac): tac'_
neuper@41990: val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions *);
neuper@41990: val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond["sqroot-test", "univariate", ...]) *);
neuper@41990: val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("End_Proof'" *);
neuper@41990: -----*)
neuper@41990: 
neuper@41990: