718 (*6>*)(*completeCalcHead*)autoCalculate 1 CompleteCalcHead; |
718 (*6>*)(*completeCalcHead*)autoCalculate 1 CompleteCalcHead; |
719 (**difference II**) |
719 (**difference II**) |
720 val ((pt,_),_) = States.get_calc 1; |
720 val ((pt,_),_) = States.get_calc 1; |
721 val PblObj {probl, meth, spec, fmz, loc, ...} = get_obj I pt []; |
721 val PblObj {probl, meth, spec, fmz, loc, ...} = get_obj I pt []; |
722 val (SOME istate, NONE) = loc; |
722 val (SOME istate, NONE) = loc; |
723 (*default_print_depth 5;*) writeln (Istate.string_of ctxt (fst istate)); (*default_print_depth 3;*) |
723 |
724 (*Pstate ([], |
724 val "Pstate ([], [], empty, NONE, \n??.empty, ORundef, false, false)" |
725 [], NONE, |
725 = fst istate |> Istate.string_of ctxt |
726 ??.empty, Sundef, false)*) |
726 val ("Isac_Knowledge", ["derivative_of", "function"], ["diff", "differentiate_on_R"]) = spec; |
727 (*default_print_depth 5;*) spec; (*default_print_depth 3;*) |
727 val "[\n(1, [1], true ,#Given, (Cor_POS functionTerm (x \<up> 2 + x + 1) , pen2str, Position.T)), \n(2, [1], true ,#Given, (Cor_POS differentiateFor x , pen2str, Position.T)), \n(3, [1], true ,#Find, (Cor_POS derivative f_'_f , pen2str, Position.T))]" |
728 (*("Isac_Knowledge", |
728 = probl |> I_Model.OLD_to_POS |> I_Model.to_string_POS ctxt |
729 ["derivative_of", "function"], |
729 val "[\n(1, [1], true ,#Given, (Cor_POS functionTerm (x \<up> 2 + x + 1) , pen2str, Position.T)), \n(2, [1], true ,#Given, (Cor_POS differentiateFor x , pen2str, Position.T)), \n(3, [1], true ,#Find, (Cor_POS derivative f_'_f , pen2str, Position.T))]" |
730 ["diff", "differentiate_on_R"]) : spec*) |
730 = meth |> I_Model.OLD_to_POS |> I_Model.to_string_POS ctxt; |
731 writeln (I_Model.to_string ctxt probl); |
731 |
732 (*[ |
|
733 (1 ,[1] ,true ,#Given ,Cor functionTerm (x \<up> 2 + x + 1) ,(f_, [x \<up> 2 + x + 1])), |
|
734 (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])), |
|
735 (3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*) |
|
736 writeln (I_Model.to_string ctxt meth); |
|
737 (*[ |
|
738 (1 ,[1] ,true ,#Given ,Cor functionTerm (x \<up> 2 + x + 1) ,(f_, [x \<up> 2 + x + 1])), |
|
739 (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])), |
|
740 (3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*) |
|
741 writeln"-----------------------------------------------------------"; |
|
742 (*7>*)fetchProposedTactic 1 (*--> Apply_Method*); |
732 (*7>*)fetchProposedTactic 1 (*--> Apply_Method*); |
743 autoCalculate 1 (Steps 1); |
733 autoCalculate 1 (Steps 1); |
744 val ((pt,p),_) = States.get_calc 1; |
734 val ((pt,p),_) = States.get_calc 1; |
745 val Form res = (#1 o (ME_Misc.pt_extract ctxt)) (pt, p); |
735 val Form res = (#1 o (ME_Misc.pt_extract ctxt)) (pt, p); |
746 if UnparseC.term @{context} res = "d_d x (x \<up> 2 + x + 1)" then () |
736 if UnparseC.term @{context} res = "d_d x (x \<up> 2 + x + 1)" then () |