agriesma@338: (* intermediately stores !ptyps
agriesma@338:    WN.16.9.01
agriesma@338:    use"tests/refine.sml";
agriesma@338:    *)
agriesma@338: 
agriesma@338: 
agriesma@338: "----------------------- store test-pbtyps ----------------------------";
agriesma@338: "----------------------- refin test-pbtyps ----------------------------";
agriesma@338: "----------------------- refine_ori test-pbtyps ----------------------------";
agriesma@338: "----------------------- refine test-pbtyps ----------------------------";
agriesma@338: "----------------------- Refine_Problem (aus subp-rooteq.sml) ---------";
agriesma@338: 
agriesma@338: 
agriesma@338: 
agriesma@338: 
agriesma@338: "----------------------- store test-pbtyps ----------------------------";
agriesma@338: val intermediate_ptyps = !ptyps;
agriesma@338: ptyps:= ([]:ptyps);
agriesma@338: 
agriesma@338: store_pbt
agriesma@338:  (prep_pbt DiffApp.thy
agriesma@338:  (["pbla"],         
agriesma@338:   [("#Given", ["fixedValues a_"])], e_rls, None, []));
agriesma@338: store_pbt
agriesma@338:  (prep_pbt DiffApp.thy
agriesma@338:  (["pbla1","pbla"], 
agriesma@338:   [("#Given", ["fixedValues a_","maximum a1_"])], e_rls, None, []));
agriesma@338: store_pbt
agriesma@338:  (prep_pbt DiffApp.thy
agriesma@338:  (["pbla2","pbla"], 
agriesma@338:   [("#Given", ["fixedValues a_","valuesFor a2_"])], e_rls, None, []));
agriesma@338: store_pbt
agriesma@338:  (prep_pbt DiffApp.thy
agriesma@338:  (["pbla2x","pbla2","pbla"],
agriesma@338:   [("#Given", ["fixedValues a_","valuesFor a2_","functionOf a2x_"])], 
agriesma@338:   e_rls, None, []));
agriesma@338: store_pbt
agriesma@338:  (prep_pbt DiffApp.thy
agriesma@338:  (["pbla2y","pbla2","pbla"],
agriesma@338:   [("#Given" ,["fixedValues a_","valuesFor a2_","boundVariable a2y_"])], 
agriesma@338:   e_rls, None, []));
agriesma@338: store_pbt
agriesma@338:  (prep_pbt DiffApp.thy
agriesma@338:  (["pbla2z","pbla2","pbla"],
agriesma@338:   [("#Given" ,["fixedValues a_","valuesFor a2_","interval a2z_"])], 
agriesma@338:   e_rls, None, []));
agriesma@338: store_pbt
agriesma@338:  (prep_pbt DiffApp.thy
agriesma@338:  (["pbla3","pbla"],
agriesma@338:   [("#Given" ,["fixedValues a_","relations a3_"])], 
agriesma@338:   e_rls, None, []));
agriesma@338: 
agriesma@338: show_ptyps();
agriesma@338: 
agriesma@338: (*case 1: no refinement *)
agriesma@338: val thy = Isac.thy;
agriesma@338: val (d1,ts1,vs1) = split_dts thy ((term_of o the o (parse thy)) 
agriesma@338: 				"fixedValues [aaa=0]");
agriesma@338: val (d2,ts2,vs2) = split_dts thy ((term_of o the o (parse thy)) 
agriesma@338: 				"errorBound (ddd=0)");
agriesma@338: val ori1 = [(1,[1],"#Given",d1,ts1),
agriesma@338: 	    (2,[1],"#Given",d2,ts2)]:ori list;
agriesma@338: 
agriesma@338: 
agriesma@338: (*case 2: refined to pbt without children *)
agriesma@338: val (d2,ts2,vs2) = split_dts thy ((term_of o the o (parse thy)) 
agriesma@338: 				"relations aaa333");
agriesma@338: val ori2 = [(1,[1],"#Given",d1,ts1),
agriesma@338: 	    (2,[1],"#Given",d2,ts2)]:ori list;
agriesma@338: 
agriesma@338: 
agriesma@338: (*case 3: refined to pbt with children *)
agriesma@338: val (d2,ts2,vs2) = split_dts thy ((term_of o the o (parse thy)) 
agriesma@338: 				"valuesFor aaa222");
agriesma@338: val ori3 = [(1,[1],"#Given",d1,ts1),
agriesma@338: 	    (2,[1],"#Given",d2,ts2)]:ori list;
agriesma@338: 
agriesma@338: 
agriesma@338: (*case 4: refined to children (without child)*)
agriesma@338: val (d3,ts3,vs3) = split_dts thy ((term_of o the o (parse thy)) 
agriesma@338: 				"boundVariable aaa222yyy");
agriesma@338: val ori4 = [(1,[1],"#Given",d1,ts1),
agriesma@338: 	    (2,[1],"#Given",d2,ts2),
agriesma@338: 	    (3,[1],"#Given",d3,ts3)]:ori list;
agriesma@338: 
agriesma@338: "----------------------- refin test-pbtyps ----------------------------";
agriesma@338: 
agriesma@338: (*case 1: no refinement *)
agriesma@338: refin [] ori1 (hd (!ptyps));
agriesma@338: (*val it = Some ["pbla"] : pblID option*)
agriesma@338: 
agriesma@338: (*case 2: refined to pbt without children *)
agriesma@338: refin [] ori2 (hd (!ptyps));
agriesma@338: (*val it = Some ["pbla","pbla3"] : pblID option*)
agriesma@338: 
agriesma@338: (*case 3: refined to pbt with children *)
agriesma@338: refin [] ori3 (hd (!ptyps));
agriesma@338: (*val it = Some ["pbla","pbla2"] : pblID option*)
agriesma@338: 
agriesma@338: (*case 4: refined to children (without child)*)
agriesma@338: refin [] ori4 (hd (!ptyps));
agriesma@338: (*val it = Some ["pbla","pbla2","pbla2y"] : pblID option*)
agriesma@338: 
agriesma@338: (*case 5: start refinement somewhere in ptyps*)
agriesma@338: val [Ptyp ("pbla",_,[_, ppp as Ptyp ("pbla2",_,_), _])] = !ptyps;
agriesma@338: refin ["pbla"] ori4 ppp;
agriesma@338: (*val it = Some ["pbla2","pbla2y"] : pblRD option*)
agriesma@338: 
agriesma@338: 
agriesma@338: "----------------------- refine_ori test-pbtyps ----------------------------";
agriesma@338: 
agriesma@338: (*case 1: no refinement *)
agriesma@338: refine_ori ori1 ["pbla"];
agriesma@338: (*val it = None : pblID option !!!!*)
agriesma@338: 
agriesma@338: (*case 2: refined to pbt without children *)
agriesma@338: refine_ori ori2 ["pbla"];
agriesma@338: (*val it = Some ["pbla3","pbla"] : pblID option*)
agriesma@338: 
agriesma@338: (*case 3: refined to pbt with children *)
agriesma@338: refine_ori ori3 ["pbla"];
agriesma@338: (*val it = Some ["pbla2","pbla"] : pblID option*)
agriesma@338: 
agriesma@338: (*case 4: refined to children (without child)*)
agriesma@338: val opt = refine_ori ori4 ["pbla"];
agriesma@338: if opt = Some ["pbla2y","pbla2","pbla"] then ()
agriesma@338: else raise error "new behaviour in refine.sml case 4";
agriesma@338: 
agriesma@338: (*case 5: start refinement somewhere in ptyps*)
agriesma@338: refine_ori ori4 ["pbla2","pbla"];
agriesma@338: (*val it = Some ["pbla2y","pbla2","pbla"] : pblID option*)
agriesma@338: 
agriesma@338: 
agriesma@338: "----------------------- refine test-pbtyps ----------------------------";
agriesma@338: 
agriesma@338: val fmz1 = ["fixedValues [aaa=0]","errorBound (ddd=0)"];
agriesma@338: val fmz2 = ["fixedValues [aaa=0]","relations aaa333"];
agriesma@338: val fmz3 = ["fixedValues [aaa=0]","valuesFor aaa222"];
agriesma@338: val fmz4 = ["fixedValues [aaa=0]","valuesFor aaa222",
agriesma@338: 	    "boundVariable aaa222yyy"];
agriesma@338: 
agriesma@338: (*case 1: no refinement *)
agriesma@338: refine fmz1 ["pbla"];
agriesma@338: (* 
agriesma@338: *** pass ["pbla"]
agriesma@338: *** pass ["pbla","pbla1"]
agriesma@338: *** pass ["pbla","pbla2"]
agriesma@338: *** pass ["pbla","pbla3"]
agriesma@338: val it =
agriesma@338:   [Matches
agriesma@338:      (["pbla"],
agriesma@338:       {Find=[],
agriesma@338:        Given=[Correct "fixedValues [aaa = #0]",
agriesma@338:               Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]}),
agriesma@338:    NoMatch
agriesma@338:      (["pbla1","pbla"],
agriesma@338:       {Find=[],
agriesma@338:        Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",
agriesma@338:               Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]}),
agriesma@338:    NoMatch
agriesma@338:      (["pbla2","pbla"],
agriesma@338:       {Find=[],
agriesma@338:        Given=[Correct "fixedValues [aaa = #0]",Missing "valuesFor a2_",
agriesma@338:               Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]}),
agriesma@338:    NoMatch
agriesma@338:      (["pbla3","pbla"],
agriesma@338:       {Find=[],
agriesma@338:        Given=[Correct "fixedValues [aaa = #0]",Missing "relations a3_",
agriesma@338:               Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]})]
agriesma@338:   : match list*)
agriesma@338: 
agriesma@338: (*case 2: refined to pbt without children *)
agriesma@338: refine fmz2 ["pbla"];
agriesma@338: (* 
agriesma@338: *** pass ["pbla"]
agriesma@338: *** pass ["pbla","pbla1"]
agriesma@338: *** pass ["pbla","pbla2"]
agriesma@338: *** pass ["pbla","pbla3"]
agriesma@338: val it =
agriesma@338:   [Matches
agriesma@338:      (["pbla"],
agriesma@338:       {Find=[],
agriesma@338:        Given=[Correct "fixedValues [aaa = #0]",Superfl "relations aaa333"],
agriesma@338:        Relate=[],Where=[],With=[]}),
agriesma@338:    NoMatch
agriesma@338:      (["pbla1","pbla"],
agriesma@338:       {Find=[],
agriesma@338:        Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",
agriesma@338:               Superfl "relations aaa333"],Relate=[],Where=[],With=[]}),
agriesma@338:    NoMatch
agriesma@338:      (["pbla2","pbla"],
agriesma@338:       {Find=[],
agriesma@338:        Given=[Correct "fixedValues [aaa = #0]",Missing "valuesFor a2_",
agriesma@338:               Superfl "relations aaa333"],Relate=[],Where=[],With=[]}),
agriesma@338:    Matches
agriesma@338:      (["pbla3","pbla"],
agriesma@338:       {Find=[],
agriesma@338:        Given=[Correct "fixedValues [aaa = #0]",Correct "relations aaa333"],
agriesma@338:        Relate=[],Where=[],With=[]})] : match list*)
agriesma@338: 
agriesma@338: (*case 3: refined to pbt with children *)
agriesma@338: refine fmz3 ["pbla"];
agriesma@338: (* 
agriesma@338: *** pass ["pbla"]
agriesma@338: *** pass ["pbla","pbla1"]
agriesma@338: *** pass ["pbla","pbla2"]
agriesma@338: *** pass ["pbla","pbla2","pbla2x"]
agriesma@338: *** pass ["pbla","pbla2","pbla2y"]
agriesma@338: *** pass ["pbla","pbla2","pbla2z"]
agriesma@338: *** pass ["pbla","pbla3"]
agriesma@338: val it =
agriesma@338:   [Matches
agriesma@338:      (["pbla"],
agriesma@338:       {Find=[],
agriesma@338:        Given=[Correct "fixedValues [aaa = #0]",Superfl "valuesFor aaa222"],
agriesma@338:        Relate=[],Where=[],With=[]}),
agriesma@338:    NoMatch
agriesma@338:      (["pbla1","pbla"],
agriesma@338:       {Find=[],
agriesma@338:        Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",
agriesma@338:               Superfl "valuesFor aaa222"],Relate=[],Where=[],With=[]}),
agriesma@338:    Matches
agriesma@338:      (["pbla2","pbla"],
agriesma@338:       {Find=[],
agriesma@338:        Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222"],
agriesma@338:        Relate=[],Where=[],With=[]}),
agriesma@338:    NoMatch
agriesma@338:      (["pbla2x","pbla2","pbla"],
agriesma@338:       {Find=[],
agriesma@338:        Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
agriesma@338:               Missing "functionOf a2x_"],Relate=[],Where=[],With=[]}),
agriesma@338:    NoMatch
agriesma@338:      (["pbla2y","pbla2","pbla"],
agriesma@338:       {Find=[],
agriesma@338:        Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
agriesma@338:               Missing "boundVariable a2y_"],Relate=[],Where=[],With=[]}),
agriesma@338:    NoMatch
agriesma@338:      (["pbla2z","pbla2","pbla"],
agriesma@338:       {Find=[],
agriesma@338:        Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
agriesma@338:               Missing "interval a2z_"],Relate=[],Where=[],With=[]}),
agriesma@338:    NoMatch
agriesma@338:      (["pbla3","pbla"],
agriesma@338:       {Find=[],
agriesma@338:        Given=[Correct "fixedValues [aaa = #0]",Missing "relations a3_",
agriesma@338:               Superfl "valuesFor aaa222"],Relate=[],Where=[],With=[]})]
agriesma@338:   : match list*)
agriesma@338: 
agriesma@338: (*case 4: refined to children (without child)*)
agriesma@338: refine fmz4 ["pbla"];
agriesma@338: (* 
agriesma@338: *** pass ["pbla"]
agriesma@338: *** pass ["pbla","pbla1"]
agriesma@338: *** pass ["pbla","pbla2"]
agriesma@338: *** pass ["pbla","pbla2","pbla2x"]
agriesma@338: *** pass ["pbla","pbla2","pbla2y"]
agriesma@338: val it =
agriesma@338:   [Matches
agriesma@338:      (["pbla"],
agriesma@338:       {Find=[],
agriesma@338:        Given=[Correct "fixedValues [aaa = #0]",Superfl "valuesFor aaa222",
agriesma@338:               Superfl "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]}),
agriesma@338:    NoMatch
agriesma@338:      (["pbla1","pbla"],
agriesma@338:       {Find=[],
agriesma@338:        Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",
agriesma@338:               Superfl "valuesFor aaa222",Superfl "boundVariable aaa222yyy"],
agriesma@338:        Relate=[],Where=[],With=[]}),
agriesma@338:    Matches
agriesma@338:      (["pbla2","pbla"],
agriesma@338:       {Find=[],
agriesma@338:        Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
agriesma@338:               Superfl "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]}),
agriesma@338:    NoMatch
agriesma@338:      (["pbla2x","pbla2","pbla"],
agriesma@338:       {Find=[],
agriesma@338:        Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
agriesma@338:               Missing "functionOf a2x_",Superfl "boundVariable aaa222yyy"],
agriesma@338:        Relate=[],Where=[],With=[]}),
agriesma@338:    Matches
agriesma@338:      (["pbla2y","pbla2","pbla"],
agriesma@338:       {Find=[],
agriesma@338:        Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
agriesma@338:               Correct "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]})]
agriesma@338:   : match list*)
agriesma@338: 
agriesma@338: (*case 5: start refinement somewhere in ptyps*)
agriesma@338: refine fmz4 ["pbla2","pbla"];
agriesma@338: (* 
agriesma@338: *** pass ["pbla","pbla2"]
agriesma@338: *** pass ["pbla","pbla2","pbla2x"]
agriesma@338: *** pass ["pbla","pbla2","pbla2y"]
agriesma@338: val it =
agriesma@338:   [Matches
agriesma@338:      (["pbla2","pbla"],
agriesma@338:       {Find=[],
agriesma@338:        Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
agriesma@338:               Superfl "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]}),
agriesma@338:    NoMatch
agriesma@338:      (["pbla2x","pbla2","pbla"],
agriesma@338:       {Find=[],
agriesma@338:        Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
agriesma@338:               Missing "functionOf a2x_",Superfl "boundVariable aaa222yyy"],
agriesma@338:        Relate=[],Where=[],With=[]}),
agriesma@338:    Matches
agriesma@338:      (["pbla2y","pbla2","pbla"],
agriesma@338:       {Find=[],
agriesma@338:        Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
agriesma@338:               Correct "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]})]
agriesma@338:   : match list*)
agriesma@338: 
agriesma@338: 
agriesma@338: ptyps:= intermediate_ptyps;
agriesma@338: show_ptyps();
agriesma@338: 
agriesma@338: 
agriesma@338: 
agriesma@338: "----------------------- Refine_Problem (aus subp-rooteq.sml) ---------";
agriesma@338: "----------------refine.sml: miniscript with mini-subpbl -------------";
agriesma@338: val fmz = ["equality ((x+1)*(x+2)=x^^^2+8)","solveFor x",
agriesma@338: 	   "errorBound (eps=0)","solutions L"];
agriesma@338: val (dI',pI',mI') = ("Test.thy",["sqroot-test","univariate","equation","test"],
agriesma@338: 		     ("Test.thy","squ-equ-test-subpbl1"));
agriesma@338: val p = e_pos'; val c = []; 
agriesma@338: val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
agriesma@338: val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p c pt;
agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p c pt;
agriesma@338: 
agriesma@338: val nxt = ("Specify_Problem",
agriesma@338: 	   Specify_Problem ["linear","univariate","equation","test"]);
agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p c pt;
agriesma@338: (*ML> f;
agriesma@338: val it = Form' (PpcKF (0,EdUndef,0,Nundef,
agriesma@338:         (Problem ["linear","univariate","equation","test"],
agriesma@338:          {Find=[Incompl "solutions []"],
agriesma@338:           Given=[Incompl "errorBound",
agriesma@338:                  Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
agriesma@338:                  Correct "solveFor x"],Relate=[],
agriesma@338:           Where=[False "matches (x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)
agriesma@338:                 |\nmatches (?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)
agriesma@338:                 |\nmatches (?a + x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)
agriesma@338:         |\nmatches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],
agriesma@338:           With=[]}))) : mout
agriesma@338: 
agriesma@338: val nxt = ("Add_Given",Add_Given "errorBound (eps = #0)")*)
agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p c pt;
agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p c pt;
agriesma@338: (*val nxt = ("Refine_Problem",Refine_Problem ["linear","univariate","equation","test"]
agriesma@338:              kann nicht gut gehen            --------- *)
agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p c pt;
agriesma@338: (*val nxt = ("Specify_Problem",Specify_Problem []) FIXXXME*)
agriesma@338: 
agriesma@338: val nxt = ("Refine_Problem",Refine_Problem ["univariate","equation","test"]);
agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p c pt;
agriesma@338: (*("Specify_Problem",Specify_Problem ["normalize","univariate","equation","test"])*)
agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p c pt;
agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p c pt;
agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p c pt;
agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p c pt;
agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p c pt;
agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p c pt;
agriesma@338: (*val nxt = ("Subproblem",Subproblem ("Test.thy",[#,#,#])) : string * mstep
agriesma@338:   in Script "uberdefiniert                         -^-*)
agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p c pt;
agriesma@338: (*val nxt = ("Model_Problem",Model_Problem ["linear","univariate","equation","test"]*)
agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p c pt;
agriesma@338: (*val nxt = ("Add_Given",Add_Given "equality (x + #1 + #-1 * #2 = #0)") *)
agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p c pt;
agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p c pt;
agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p c pt;
agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p c pt;
agriesma@338: (*("Specify_Problem",Specify_Problem ["linear","univariate","equation","test"])*)
agriesma@338: 
agriesma@338: val nxt = ("Refine_Problem",Refine_Problem ["univariate","equation","test"]);
agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p c pt;
agriesma@338: (*val nxt = ("Specify_Method",Specify_Method ("RatArith.thy","solve_linear"))*)
agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p c pt;
agriesma@338: (*val nxt = ("Apply_Method",Apply_Method ("RatArith.thy","solve_linear"))*)
agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p c pt;
agriesma@338: (*val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst ([#],"isolate_bdv"))*)
agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p c pt;
agriesma@338: (*val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify")*)
agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p c pt;
agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p c pt;
agriesma@338: (*val nxt = ("Check_Postcond",Check_Postcond ["linear","univariate","eq*)
agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p c pt;
agriesma@338: (*val nxt = ("Check_elementwise",Check_elementwise "Assumptions")*)
agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p c pt;
agriesma@338: (*("Check_Postcond",Check_Postcond ["normalize","univariate","equation","test"])*)
agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p c pt;
agriesma@338: val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
agriesma@338: if (snd nxt)=End_Proof' andalso res="[x = 2]" then ()
agriesma@338: else raise error "new behaviour in test:refine.sml: miniscript with mini-subpbl";
agriesma@338: 
agriesma@338: