Mercurial Mercurial > wneuper > isa / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/Knowledge/rootrateq.sml
branchisac-update-Isa09-2
changeset 37991 028442673981
parent 37960 ec20007095f2
child 38031 460c24a6a6ba
equal deleted inserted replaced
37990:24609758d219 37991:028442673981 
    48  else  raise error "rootrateq.sml: diff.behav. 7 in is_rootRatAddTerm_in";
 
    48  else  raise error "rootrateq.sml: diff.behav. 7 in is_rootRatAddTerm_in";
 
    49 
    49 
    50 
    50 
    51 "--------------------- test thm rootrat_equation_left_1 ---------------------";
 
    51 "--------------------- test thm rootrat_equation_left_1 ---------------------";
 
    52 val fmz = ["equality ( -2 + 1/(1 - sqrt(x))= 0)", "solveFor x","solutions L"];
 
    52 val fmz = ["equality ( -2 + 1/(1 - sqrt(x))= 0)", "solveFor x","solutions L"];
 
    53 val (dI',pI',mI') = ("RootRatEq.thy",["univariate","equation"],["no_met"]);
 
    53 val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]);
 
    54 
    54 
    55 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
    55 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
    56 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    56 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    57 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    57 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    58 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    58 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    59 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    59 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    60 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    60 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    61 val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    61 val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    62 (*-> Subproblem ("RootEq.thy", ["univariate", ...])*)
 
    62 (*-> Subproblem ("RootEq", ["univariate", ...])*)
 
    63 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    63 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    64 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    64 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    65 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    65 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    66 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    66 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    67 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    67 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    68 val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    68 val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    69 (*-> Subproblem ("RootEq.thy", ["univariate", ...])*)
 
    69 (*-> Subproblem ("RootEq", ["univariate", ...])*)
 
    70 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    70 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    71 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    71 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    72 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    72 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    73 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    73 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    74 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    74 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    75 val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    75 val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    76 (*-> Subproblem ("RootEq.thy", ["univariate", ...])*)
 
    76 (*-> Subproblem ("RootEq", ["univariate", ...])*)
 
    77 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    77 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    78 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    78 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    79 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    79 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    80 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    80 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    81 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    81 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    82 val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    82 val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    83 if f =  Form' (FormKF (~1, EdUndef, 0, Nundef, "1 + -4 * x = 0")) then ()
 
    83 if f =  Form' (FormKF (~1, EdUndef, 0, Nundef, "1 + -4 * x = 0")) then ()
 
    84 else raise error "rootrateq.sml: diff.behav. in rootrat_equation_left_1";
 
    84 else raise error "rootrateq.sml: diff.behav. in rootrat_equation_left_1";
 
    85 (*-> Subproblem ("RootEq.thy", ["polynomial", ...])*)
 
    85 (*-> Subproblem ("RootEq", ["polynomial", ...])*)
 
    86 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    86 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    87 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    87 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    88 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    88 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    89 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    89 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    90 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    90 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    96 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 4]")) => ()
 
    96 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 4]")) => ()
 
    97 	 | _ => raise error "rootrateq.sml: diff.behav. in  -2 + 1/(1 - sqrt(x))= 0 -> [x = 1/4]";
 
    97 	 | _ => raise error "rootrateq.sml: diff.behav. in  -2 + 1/(1 - sqrt(x))= 0 -> [x = 1/4]";
 
    98 
    98 
    99 "--------------------- test thm rootrat_equation_left_2 ---------------------";
 
    99 "--------------------- test thm rootrat_equation_left_2 ---------------------";
 
   100 val fmz = ["equality (3/(1+sqrt(x))= 1)", "solveFor x","solutions L"];
 
   100 val fmz = ["equality (3/(1+sqrt(x))= 1)", "solveFor x","solutions L"];
 
   101 val (dI',pI',mI') = ("RootRatEq.thy",["univariate","equation"],["no_met"]);
 
   101 val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]);
 
   102 
   102 
   103 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   103 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   104 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   104 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   105 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   105 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   106 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   106 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   107 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   107 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   108 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   108 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   109 (*-> Subproblem ("RootEq.thy", ["univariate", ...])*)
 
   109 (*-> Subproblem ("RootEq", ["univariate", ...])*)
 
   110 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   110 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   111 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   111 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   112 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   112 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   113 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   113 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   114 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   114 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   115 val (p,_,f,nxt,_,pt) = me nxt p c pt; 
   115 val (p,_,f,nxt,_,pt) = me nxt p c pt; 
   116 (*-> Subproblem ("RootEq.thy", ["univariate", ...])*)
 
   116 (*-> Subproblem ("RootEq", ["univariate", ...])*)
 
   117 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   117 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   118 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   118 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   119 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   119 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   120 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   120 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   121 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   121 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   122 val (p,_,f,nxt,_,pt) = me nxt p c pt; 
   122 val (p,_,f,nxt,_,pt) = me nxt p c pt; 
   123 (*-> Subproblem ("RootEq.thy", ["univariate", ...])*)
 
   123 (*-> Subproblem ("RootEq", ["univariate", ...])*)
 
   124 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   124 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   125 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   125 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   126 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   126 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   127 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   127 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   128 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   128 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   129 val (p,_,f,nxt,_,pt) = me nxt p c pt; 
   129 val (p,_,f,nxt,_,pt) = me nxt p c pt; 
   130 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "4 + -1 * x = 0")) then ()
 
   130 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "4 + -1 * x = 0")) then ()
 
   131 else raise error "rootrateq.sml: diff.behav. in rootrat_equation_left_2";
 
   131 else raise error "rootrateq.sml: diff.behav. in rootrat_equation_left_2";
 
   132 (*-> Subproblem ("PolyEq.thy", ["polynomial", ...])*)
 
   132 (*-> Subproblem ("PolyEq", ["polynomial", ...])*)
 
   133 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   133 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   134 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   134 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   135 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   135 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   136 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   136 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   137 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   137 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   143 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]")) => ()
 
   143 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]")) => ()
 
   144 	 | _ => raise error "rootrateq.sml: diff.behav. in  3/(1+sqrt(x))= 1 -> [x = 4]";
 
   144 	 | _ => raise error "rootrateq.sml: diff.behav. in  3/(1+sqrt(x))= 1 -> [x = 4]";
 
   145 
   145 
   146 "--------------------- test thm rootrat_equation_right_1 ---------------";
 
   146 "--------------------- test thm rootrat_equation_right_1 ---------------";
 
   147 val fmz = ["equality ( 0= -2 + 1/(1 - sqrt(x)))", "solveFor x","solutions L"];
 
   147 val fmz = ["equality ( 0= -2 + 1/(1 - sqrt(x)))", "solveFor x","solutions L"];
 
   148 val (dI',pI',mI') = ("RootRatEq.thy",["univariate","equation"],["no_met"]);
 
   148 val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]);
 
   149 
   149 
   150 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   150 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   151 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   151 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   152 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   152 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   153 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   153 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   186 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 4]")) => ()
 
   186 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 4]")) => ()
 
   187 	 | _ => raise error "rootrateq.sml: diff.behav. in  -2 + 1/(1 - sqrt(x))= 0 -> [x = 1/4]";
 
   187 	 | _ => raise error "rootrateq.sml: diff.behav. in  -2 + 1/(1 - sqrt(x))= 0 -> [x = 1/4]";
 
   188 
   188 
   189 "--------------------- test thm rootrat_equation_right_2 --------------------";
 
   189 "--------------------- test thm rootrat_equation_right_2 --------------------";
 
   190 val fmz = ["equality (1 = 3/(1+sqrt(x)))", "solveFor x","solutions L"];
 
   190 val fmz = ["equality (1 = 3/(1+sqrt(x)))", "solveFor x","solutions L"];
 
   191 val (dI',pI',mI') = ("RootRatEq.thy",["univariate","equation"],["no_met"]);
 
   191 val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]);
 
   192 
   192 
   193 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   193 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   194 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   194 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   195 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   195 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   196 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   196 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper/isa