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/Interpret/calchead.sml
changeset 59267 aab874fdd910
parent 59265 ee68ccda7977
child 59279 255c853ea2f0
equal deleted inserted replaced
59266:56762e8a672e 59267:aab874fdd910 
    78    ["DiffApp","max_by_calculus"]);
 
    78    ["DiffApp","max_by_calculus"]);
 
    79 val c = []:cid;
 
    79 val c = []:cid;
 
    80 
    80 
    81 val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
    81 val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
    82 val nxt = tac2tac_ pt p nxt; 
    82 val nxt = tac2tac_ pt p nxt; 
    83 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
 
    83 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
 
    84 (*val nxt = Add_Given "fixedValues [(r::real) = Arbfix]" : tac*)
 
    84 (*val nxt = Add_Given "fixedValues [(r::real) = Arbfix]" : tac*)
 
    85 
    85 
    86 val nxt = tac2tac_ pt p nxt; 
    86 val nxt = tac2tac_ pt p nxt; 
    87 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
 
    87 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
 
    88 (**)
 
    88 (**)
 
    89 
    89 
    90 val nxt = tac2tac_ pt p (Add_Find "valuesFor [(a::real)]"); 
    90 val nxt = tac2tac_ pt p (Add_Find "valuesFor [(a::real)]"); 
    91 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
 
    91 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
 
    92 if ppc<>(Problem [],  
    92 if ppc<>(Problem [],  
    93          {Find=[Incompl "maximum",Incompl "valuesFor [a]"],
 
    93          {Find=[Incompl "maximum",Incompl "valuesFor [a]"],
 
    94 	  Given=[Correct "fixedValues [r = Arbfix]"],
 
    94 	  Given=[Correct "fixedValues [r = Arbfix]"],
 
    95 	  Relate=[Incompl "relations"], Where=[],With=[]})
 
    95 	  Relate=[Incompl "relations"], Where=[],With=[]})
 
    96 then error "test-maximum.sml: model stepwise - different behaviour" 
    96 then error "test-maximum.sml: model stepwise - different behaviour" 
   100 (* WN1130630 THE maximum example WORKS IN isabisac09-2; 
   100 (* WN1130630 THE maximum example WORKS IN isabisac09-2; 
   101   MOST LIKELY IT IS BROKEN BY INTRODUCING  ctxt. 
   101   MOST LIKELY IT IS BROKEN BY INTRODUCING  ctxt. 
   102   Some tests have been broken much earlier, 
   102   Some tests have been broken much earlier, 
   103   see test/../calchead.sml "inhibit exn 010830". *)
 
   103   see test/../calchead.sml "inhibit exn 010830". *)
 
   104 (*========== inhibit exn WN1130630 maximum example broken =========================
 
   104 (*========== inhibit exn WN1130630 maximum example broken =========================
 
   105 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
 
   105 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
 
   106 ============ inhibit exn WN1130630 maximum example broken =======================*)
 
   106 ============ inhibit exn WN1130630 maximum example broken =======================*)
 
   107 
   107 
   108 val nxt = tac2tac_ pt p (Add_Given "boundVariable a+"); 
   108 val nxt = tac2tac_ pt p (Add_Given "boundVariable a+"); 
   109 (*========== inhibit exn WN1130630 maximum example broken =========================
 
   109 (*========== inhibit exn WN1130630 maximum example broken =========================
 
   110 (* ERROR: Exception Bind raised *)
 
   110 (* ERROR: Exception Bind raised *)
 
   111 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
 
   111 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
 
   112 ============ inhibit exn WN1130630 maximum example broken =======================*)
 
   112 ============ inhibit exn WN1130630 maximum example broken =======================*)
 
   113 
   113 
   114 val m = Specify_Problem ["maximum_of","function"];
 
   114 val m = Specify_Problem ["maximum_of","function"];
 
   115 val nxt = tac2tac_ pt p m; 
   115 val nxt = tac2tac_ pt p m; 
   116 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
 
   116 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
 
   117 (*========== inhibit exn WN1130630 maximum example broken =========================
 
   117 (*========== inhibit exn WN1130630 maximum example broken =========================
 
   118 if ppc<>(Problem ["maximum_of","function"],  
   118 if ppc<>(Problem ["maximum_of","function"],  
   119          {Find=[Incompl "maximum",Incompl "valuesFor"],
 
   119          {Find=[Incompl "maximum",Incompl "valuesFor"],
 
   120 	  Given=[Correct "fixedValues [r = Arbfix]"],
 
   120 	  Given=[Correct "fixedValues [r = Arbfix]"],
 
   121 	  Relate=[Incompl "relations []"], Where=[],With=[]})
 
   121 	  Relate=[Incompl "relations []"], Where=[],With=[]})
 
   129 then error "diffappl.sml: Specify_Problem different behaviour" 
   129 then error "diffappl.sml: Specify_Problem different behaviour" 
   130 else ();*)
 
   130 else ();*)
 
   131 ============ inhibit exn WN1130630 maximum example broken =======================*)
 
   131 ============ inhibit exn WN1130630 maximum example broken =======================*)
 
   132 
   132 
   133 val nxt = tac2tac_ pt p(Specify_Method ["DiffApp","max_by_calculus"]);
 
   133 val nxt = tac2tac_ pt p(Specify_Method ["DiffApp","max_by_calculus"]);
 
   134 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
 
   134 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
 
   135 (*========== inhibit exn WN1130630 maximum example broken =========================
 
   135 (*========== inhibit exn WN1130630 maximum example broken =========================
 
   136 if ppc<>(Method ["DiffApp","max_by_calculus"],
 
   136 if ppc<>(Method ["DiffApp","max_by_calculus"],
 
   137 	 {Find=[Incompl "maximum",Incompl "valuesFor"],
 
   137 	 {Find=[Incompl "maximum",Incompl "valuesFor"],
 
   138 	  Given=[Correct "fixedValues [r = Arbfix]",Missing "boundVariable v_v",
 
   138 	  Given=[Correct "fixedValues [r = Arbfix]",Missing "boundVariable v_v",
 
   139 		 Missing "interval itv_",Missing "errorBound err_"],
 
   139 		 Missing "interval itv_",Missing "errorBound err_"],
 
   171 val c = []:cid;
 
   171 val c = []:cid;
 
   172 (*val nxt = Init_Proof' (fmz,(dI',pI',mI'));*)
 
   172 (*val nxt = Init_Proof' (fmz,(dI',pI',mI'));*)
 
   173 val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   173 val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   174 
   174 
   175 val nxt = tac2tac_ pt p nxt; 
   175 val nxt = tac2tac_ pt p nxt; 
   176 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt e_pos' [] pt;
 
   176 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt e_pos' [] pt;
 
   177 val nxt = tac2tac_ pt p nxt; 
   177 val nxt = tac2tac_ pt p nxt; 
   178 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
 
   178 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
 
   179 (*val nxt = Add_Given "fixedValues [(r::real) = Arbfix]" : tac*)
 
   179 (*val nxt = Add_Given "fixedValues [(r::real) = Arbfix]" : tac*)
 
   180 
   180 
   181 val nxt = tac2tac_ pt p nxt; 
   181 val nxt = tac2tac_ pt p nxt; 
   182 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
 
   182 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
 
   183 (*val nxt = Add_Find "maximum (A::bool)" : tac*)
 
   183 (*val nxt = Add_Find "maximum (A::bool)" : tac*)
 
   184 
   184 
   185 val nxt = tac2tac_ pt p nxt; 
   185 val nxt = tac2tac_ pt p nxt; 
   186 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
 
   186 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
 
   187 (*val nxt = Add_Find "valuesFor [(a::real)]" : tac*)
 
   187 (*val nxt = Add_Find "valuesFor [(a::real)]" : tac*)
 
   188 
   188 
   189 val nxt = tac2tac_ pt p nxt; 
   189 val nxt = tac2tac_ pt p nxt; 
   190 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
 
   190 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
 
   191 (*val nxt = Add_Find "valuesFor [(b::real)]" : tac*)
 
   191 (*val nxt = Add_Find "valuesFor [(b::real)]" : tac*)
 
   192 
   192 
   193 val nxt = tac2tac_ pt p nxt; 
   193 val nxt = tac2tac_ pt p nxt; 
   194 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
 
   194 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
 
   195 (*val nxt = Add_Relation "relations [A = a * b]" *)
 
   195 (*val nxt = Add_Relation "relations [A = a * b]" *)
 
   196 
   196 
   197 val nxt = tac2tac_ pt p nxt; 
   197 val nxt = tac2tac_ pt p nxt; 
   198 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
 
   198 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
 
   199 (*Add_Relation "relations\n [((a::real) // (#2::real)) ..."*)
 
   199 (*Add_Relation "relations\n [((a::real) // (#2::real)) ..."*)
 
   200 
   200 
   201 (*---------------------------- FIXXXXME.meNEW !!! partial Add-Relation !!!
 
   201 (*---------------------------- FIXXXXME.meNEW !!! partial Add-Relation !!!
 
   202   nxt_specif <> specify ?!
 
   202   nxt_specif <> specify ?!
 
   203 
   203 
   204 if nxt<>(Add_Relation 
   204 if nxt<>(Add_Relation 
   205  "relations [(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]")
 
   205  "relations [(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]")
 
   206 then error "test specify, fmz <> []: nxt <> Add_Relation (a/2)^2.." else (); (*different with show_types !!!*)
 
   206 then error "test specify, fmz <> []: nxt <> Add_Relation (a/2)^2.." else (); (*different with show_types !!!*)
 
   207 
   207 
   208 val nxt = tac2tac_ pt p nxt; 
   208 val nxt = tac2tac_ pt p nxt; 
   209 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
 
   209 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
 
   210 ------------------------------ FIXXXXME.meNEW !!! ---*)
 
   210 ------------------------------ FIXXXXME.meNEW !!! ---*)
 
   211 
   211 
   212 (*val nxt = Specify_Theory "DiffApp" : tac*)
 
   212 (*val nxt = Specify_Theory "DiffApp" : tac*)
 
   213 
   213 
   214 val itms = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt itms);
 
   214 val itms = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt itms);
 
   215 
   215 
   216 val nxt = tac2tac_ pt p nxt; 
   216 val nxt = tac2tac_ pt p nxt; 
   217 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
 
   217 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
 
   218 (*val nxt = Specify_Problem ["maximum_of","function"]*)
 
   218 (*val nxt = Specify_Problem ["maximum_of","function"]*)
 
   219 
   219 
   220 val nxt = tac2tac_ pt p nxt; 
   220 val nxt = tac2tac_ pt p nxt; 
   221 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
 
   221 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
 
   222 (*val nxt = Specify_Method ("DiffApp","max_by_calculus")*)
 
   222 (*val nxt = Specify_Method ("DiffApp","max_by_calculus")*)
 
   223 
   223 
   224 val nxt = tac2tac_ pt p nxt; 
   224 val nxt = tac2tac_ pt p nxt; 
   225 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
 
   225 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
 
   226 (*val nxt = Add_Given "boundVariable a" : tac*)
 
   226 (*val nxt = Add_Given "boundVariable a" : tac*)
 
   227 
   227 
   228 val nxt = tac2tac_ pt p nxt; 
   228 val nxt = tac2tac_ pt p nxt; 
   229 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
 
   229 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
 
   230 (*val nxt = Add_Given "interval {x. #0 <= x & x <= #2 * r}" : *)
 
   230 (*val nxt = Add_Given "interval {x. #0 <= x & x <= #2 * r}" : *)
 
   231 
   231 
   232 val nxt = tac2tac_ pt p nxt; 
   232 val nxt = tac2tac_ pt p nxt; 
   233 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
 
   233 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
 
   234 (*val nxt = Add_Given "errorBound (eps = #0)" : tac*)
 
   234 (*val nxt = Add_Given "errorBound (eps = #0)" : tac*)
 
   235 
   235 
   236 val nxt = tac2tac_ pt p nxt; 
   236 val nxt = tac2tac_ pt p nxt; 
   237 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
 
   237 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
 
   238 (*val nxt = Apply_Method ("DiffApp","max_by_calculus") *)
 
   238 (*val nxt = Apply_Method ("DiffApp","max_by_calculus") *)
 
   239 case nxt of (Apply_Method ["DiffApp","max_by_calculus"]) => ()
 
   239 case nxt of (Apply_Method ["DiffApp","max_by_calculus"]) => ()
 
   240 | _ => error "test specify, fmz <> []: nxt <> Apply_Method max_by_calculus";
 
   240 | _ => error "test specify, fmz <> []: nxt <> Apply_Method max_by_calculus";
 
   241 
   241 
   242 
   242 
   247 val (dI',pI',mI') = empty_spec;
 
   247 val (dI',pI',mI') = empty_spec;
 
   248 val c = []:cid;
 
   248 val c = []:cid;
 
   249 
   249 
   250 val nxt = Init_Proof' (fmz,(dI',pI',mI'));(*!!!!!!!!*)
 
   250 val nxt = Init_Proof' (fmz,(dI',pI',mI'));(*!!!!!!!!*)
 
   251 (*val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; !!!*)
 
   251 (*val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; !!!*)
 
   252 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt e_pos' [] 
   252 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt e_pos' [] 
   253   EmptyPtree;
 
   253   EmptyPtree;
 
   254 val nxt = tac2tac_ pt p nxt; 
   254 val nxt = tac2tac_ pt p nxt; 
   255 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
 
   255 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
 
   256 (*val nxt = Specify_Theory "e_domID" : tac*)
 
   256 (*val nxt = Specify_Theory "e_domID" : tac*)
 
   257 
   257 
   258 val nxt = Specify_Theory "DiffApp";
 
   258 val nxt = Specify_Theory "DiffApp";
 
   259 val nxt = tac2tac_ pt p nxt; 
   259 val nxt = tac2tac_ pt p nxt; 
   260 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
 
   260 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
 
   261 (*val nxt = Specify_Problem ["e_pblID"] : tac*)
 
   261 (*val nxt = Specify_Problem ["e_pblID"] : tac*)
 
   262 
   262 
   263 val nxt = Specify_Problem ["maximum_of","function"];
 
   263 val nxt = Specify_Problem ["maximum_of","function"];
 
   264 val nxt = tac2tac_ pt p nxt; 
   264 val nxt = tac2tac_ pt p nxt; 
   265 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
 
   265 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
 
   266 (*val nxt = Add_Given "fixedValues" : tac*)
 
   266 (*val nxt = Add_Given "fixedValues" : tac*)
 
   267 
   267 
   268 val nxt = Add_Given "fixedValues [r=Arbfix]";
 
   268 val nxt = Add_Given "fixedValues [r=Arbfix]";
 
   269 val nxt = tac2tac_ pt p nxt; 
   269 val nxt = tac2tac_ pt p nxt; 
   270 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
 
   270 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
 
   271 (*val nxt = Add_Find "maximum" : tac*)
 
   271 (*val nxt = Add_Find "maximum" : tac*)
 
   272 
   272 
   273 val nxt = Add_Find "maximum A";
 
   273 val nxt = Add_Find "maximum A";
 
   274 val nxt = tac2tac_ pt p nxt; 
   274 val nxt = tac2tac_ pt p nxt; 
   275 
   275 
   276 
   276 
   277 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
 
   277 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
 
   278 (*val nxt = Add_Find "valuesFor" : tac*)
 
   278 (*val nxt = Add_Find "valuesFor" : tac*)
 
   279 
   279 
   280 val nxt = Add_Find "valuesFor [a]";
 
   280 val nxt = Add_Find "valuesFor [a]";
 
   281 val nxt = tac2tac_ pt p nxt; 
   281 val nxt = tac2tac_ pt p nxt; 
   282 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
 
   282 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
 
   283 (*val nxt = Add_Relation "relations" --- 
   283 (*val nxt = Add_Relation "relations" --- 
   284   --- [b=Arbfix] KANN NICHT VERLANGT WERDEN !!!!*)
 
   284   --- [b=Arbfix] KANN NICHT VERLANGT WERDEN !!!!*)
 
   285 
   285 
   286 (*========== inhibit exn 010830 =======================================================*)
 
   286 (*========== inhibit exn 010830 =======================================================*)
 
   287 (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....
 
   287 (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....
 
   291 *)
 
   291 *)
 
   292 (*========== inhibit exn 010830 =======================================================*)
 
   292 (*========== inhibit exn 010830 =======================================================*)
 
   293 
   293 
   294 val nxt = Add_Relation "relations [(A=a+b)]";
 
   294 val nxt = Add_Relation "relations [(A=a+b)]";
 
   295 val nxt = tac2tac_ pt p nxt; 
   295 val nxt = tac2tac_ pt p nxt; 
   296 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
 
   296 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
 
   297 (*val nxt = Specify_Method ("e_domID","e_metID") : tac*)
 
   297 (*val nxt = Specify_Method ("e_domID","e_metID") : tac*)
 
   298 
   298 
   299 val nxt = Specify_Method ["DiffApp","max_by_calculus"];
 
   299 val nxt = Specify_Method ["DiffApp","max_by_calculus"];
 
   300 val nxt = tac2tac_ pt p nxt; 
   300 val nxt = tac2tac_ pt p nxt; 
   301 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
 
   301 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
 
   302 (*val nxt = Add_Given "boundVariable" : tac*)
 
   302 (*val nxt = Add_Given "boundVariable" : tac*)
 
   303 
   303 
   304 val nxt = Add_Given "boundVariable alpha";
 
   304 val nxt = Add_Given "boundVariable alpha";
 
   305 val nxt = tac2tac_ pt p nxt; 
   305 val nxt = tac2tac_ pt p nxt; 
   306 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
 
   306 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
 
   307 (*val nxt = Add_Given "interval" : tac*)
 
   307 (*val nxt = Add_Given "interval" : tac*)
 
   308 
   308 
   309 val nxt = Add_Given "interval {x. 2 <= x & x <= 3}";
 
   309 val nxt = Add_Given "interval {x. 2 <= x & x <= 3}";
 
   310 val nxt = tac2tac_ pt p nxt; 
   310 val nxt = tac2tac_ pt p nxt; 
   311 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
 
   311 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
 
   312 (*val nxt = Add_Given "errorBound" : tac*)
 
   312 (*val nxt = Add_Given "errorBound" : tac*)
 
   313 
   313 
   314 val nxt = Add_Given "errorBound (eps=999)";
 
   314 val nxt = Add_Given "errorBound (eps=999)";
 
   315 val nxt = tac2tac_ pt p nxt; 
   315 val nxt = tac2tac_ pt p nxt; 
   316 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
 
   316 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
 
   317 (*val nxt = Apply_Method ("DiffApp","max_by_calculus") *)
 
   317 (*val nxt = Apply_Method ("DiffApp","max_by_calculus") *)
 
   318 
   318 
   319 (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....
 
   319 (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....
 
   320 if nxt<>(Apply_Method ("DiffApp","max_by_calculus"))
 
   320 if nxt<>(Apply_Method ("DiffApp","max_by_calculus"))
 
   321 then error "test specify, fmz <> []: nxt <> Add_Relation.." 
   321 then error "test specify, fmz <> []: nxt <> Add_Relation.." 
   322 else ();
 
   322 else ();
 
   323 *)
 
   323 *)
 
   324 (* 2.4.00 nach Transfer specify -> hard_gen
 
   324 (* 2.4.00 nach Transfer specify -> hard_gen
 
   325 val nxt = Apply_Method ("DiffApp","max_by_calculus");
 
   325 val nxt = Apply_Method ("DiffApp","max_by_calculus");
 
   326 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; *)
 
   326 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt; *)
 
   327 (*val nxt = Empty_Tac : tac*)
 
   327 (*val nxt = Empty_Tac : tac*)
 
   328 
   328 
   329 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
 
   329 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
 
   330 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
 
   330 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
 
   331 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
 
   331 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
wneuper/isa