test/Tools/isac/Knowledge/diffapp.sml
branchdecompose-isar
changeset 42166 911c49949ba9
parent 41943 f33f6959948b
child 42195 ac2c5fb8fedd
     1.1 --- a/test/Tools/isac/Knowledge/diffapp.sml	Thu Jul 21 12:01:56 2011 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/diffapp.sml	Fri Jul 22 14:01:09 2011 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4  "---------------------- 2.5.03: Make_fun_by_new_variable -----------------";
     1.5  
     1.6  
     1.7 -(*=== inhibit exn ?=============================================================
     1.8 +(*=== inhibit exn 110722=============================================================
     1.9  
    1.10  
    1.11  
    1.12 @@ -112,6 +112,7 @@
    1.13       "additionalRels [(a/2)^^^2 + (b/2)^^^2 = r^^^2]"];
    1.14  map (the o (parseold thy)) fmz1;
    1.15  
    1.16 +=== inhibit exn 110722=============================================================*)
    1.17  
    1.18  
    1.19  "-------------------- ptree of {(a,b). is-max ... --------------------------";
    1.20 @@ -271,6 +272,7 @@
    1.21     ["DiffApp","max_by_calculus"]);
    1.22  
    1.23  val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    1.24 +(*=== inhibit exn 110722=============================================================
    1.25  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.26  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.27  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.28 @@ -294,6 +296,7 @@
    1.29  case nxt of (_,Apply_Method ["DiffApp","max_by_calculus"] ) => ()
    1.30  	  | _ => error "diffapp.sml: max-exp me, nxt = Apply_Method";
    1.31  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.32 +=== inhibit exn 110722=============================================================*)
    1.33  
    1.34  (*since 0508 Apply_Method does the 1st step, if NONE init_form -------------
    1.35  (*val nxt = ("Subproblem",Subproblem ("DiffApp",["make","function"]))*)
    1.36 @@ -305,21 +308,25 @@
    1.37  case nxt of (_, Model_Problem(*["by_explicit", "make", "function"]*)) => ()
    1.38  	  | _ => error "diffapp.sml: max-exp me, nxt = Model_Problem";
    1.39  
    1.40 +(*=== inhibit exn 110722=============================================================
    1.41  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.42  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.43  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.44  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.45  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.46 +=== inhibit exn 110722=============================================================*)
    1.47  
    1.48  val oris = fst3 (get_obj g_origin pt (fst p));writeln(oris2str oris);
    1.49  val pits = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt pits);
    1.50  
    1.51 +(*=== inhibit exn 110722=============================================================
    1.52  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.53  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.54  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.55  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.56  case nxt of (_, Apply_Method ["DiffApp", "make_fun_by_explicit"]) => ()
    1.57  	  | _ => error "diffapp.sml: max-exp Apply_Method ([1], Met) ";
    1.58 +=== inhibit exn 110722=============================================================*)
    1.59  
    1.60  (*----since WN050901 (ie. corr. mathengine#nxt_specify_ ..nxt_spec Pbl->p_
    1.61  we get at ...
    1.62 @@ -372,9 +379,11 @@
    1.63  Error' (Error_ "Refine_Tacitly [\"univariate\",\"equation\"] not applicable")*)
    1.64  
    1.65  
    1.66 -(*----postponed.15.5.03 run scripts for maximum-example: univariate equation
    1.67 +(*----postponed.15.5.03 run scripts for maximum-example: univariate equation*)
    1.68 +(*=== inhibit exn 110722=============================================================
    1.69  
    1.70  val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => OldGoals.print_exn e; 
    1.71 +=== inhibit exn 110722=============================================================*)
    1.72  
    1.73  val oris = fst3 (get_obj g_origin pt (fst p));writeln(oris2str oris);
    1.74  
    1.75 @@ -384,11 +393,13 @@
    1.76  val mits = get_obj g_met pt (fst p);writeln(itms2str_ ctxt mits);
    1.77  val mits = get_obj g_met pt [];writeln(itms2str_ ctxt mits);
    1.78  
    1.79 +(*=== inhibit exn 110722=============================================================
    1.80  itms2args thy ["DiffApp","max_by_calculus"] mits;
    1.81  
    1.82  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.83 +=== inhibit exn 110722=============================================================*)
    1.84  
    1.85 ----*)
    1.86 +(*---*)
    1.87  
    1.88  "--------- autoCalc .. scripts for maximum-example ---------------";
    1.89  "--------- autoCalc .. scripts for maximum-example ---------------";
    1.90 @@ -439,6 +450,7 @@
    1.91  *)
    1.92  
    1.93  
    1.94 +(*=== inhibit exn 110722=============================================================
    1.95  
    1.96  "--------------------- 30.4.03: maximum .. rewrite_set_ list_rls ---------";
    1.97  "--------------------- 30.4.03: maximum .. rewrite_set_ list_rls ---------";
    1.98 @@ -749,6 +761,4 @@
    1.99  
   1.100  
   1.101  
   1.102 -
   1.103 -
   1.104 -===== inhibit exn ?===========================================================*)
   1.105 +===== inhibit exn 110722===========================================================*)