\<close> ML \<open> (*------------- continuing XXXXX ------------------------------------------------------*)

 \<close> ML \<open> (*||----------- continuing XXXXX ------------------------------------------------------*)

 (*-------------------- continuing XXXXX ------------------------------------------------------*)

 (*||------------------ continuing XXXXX ------------------------------------------------------*)

 \<close> ML \<open>

 section \<open>===== simplify.sml ================================================================\<close>

 section \<open>===== biegelinie-2.sml ============================================================\<close>

 (* Title:  Knowledge/biegelinie-2.sml

 \<close> ML \<open>

    author: Walther Neuper 190515

 \<close> ML \<open>

    (c) due to copyright terms

 \<close>

 *)

 section \<open>===================================================================================\<close>

 section \<open>===== Interpret/li-tool.sml =======================================================\<close>

 ML \<open>

 \<close> ML \<open>

 (* Title:  Interpret/li-tool.sml

    Author: Walther Neuper 050908

    (c) copyright due to lincense terms.

 *)

 "-----------------------------------------------------------------";

 "----------- fun implicit_take, fun get_first_argument -------------------------";

 "----------- auto SubProblem (_,[vonBelastungZu,Biegelinien] -----";

 "----------- fun from_prog ---------------------------------------";

 "----------- me SubProblem (_,[vonBelastungZu,Biegelinien] -------";

 "----------- fun specific_from_prog ----------------------------";

 "----------- fun de_esc_underscore -------------------------------";

 "----------- fun go ----------------------------------------------";

 "----------- fun formal_args -------------------------------------";

 "----------- fun dsc_valT ----------------------------------------";

 "----------- fun arguments_from_model ---------------------------------------";

 "----------- fun init_pstate -----------------------------------------------------------------";

 val thy =  @{theory Isac_Knowledge};

 "----------- auto SubProblem (_,[vonBelastungZu,Biegelinien] -----";

 \<close> ML \<open>

 "----------- auto SubProblem (_,[vonBelastungZu,Biegelinien] -----";

 "----------- fun init_pstate -----------------------------------------------------------------";

 "----------- auto SubProblem (_,[vonBelastungZu,Biegelinien] -----";

 "----------- fun init_pstate -----------------------------------------------------------------";

 val fmz = 

 "----------- fun init_pstate -----------------------------------------------------------------";

     ["Streckenlast q_0", "FunktionsVariable x",

 (*

      "Funktionen [Q x = c + - 1 * q_0 * x, \

   This test is deeply nested (down into details of creating environments).

      \M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\

   In order to make Sidekick show the structure add to each

      \ y' x = c_3 + 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\

   *                    (*/...\*) and        (*\.../*)

      \ y x = c_4 + c_3 * x + 1 / (- 1 * EI) * (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]",

   * a companion  > ML < (*/...\*) and > ML < (*\.../*)

     "AbleitungBiegelinie dy"];

   Note the wrong ^----^ delimiters.

 val (dI',pI',mI') = ("Biegelinie", ["vonBelastungZu", "Biegelinien"],

 *)

 		     ["Biegelinien", "ausBelastung"]);

 val fmz = ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",

 	     "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",

 States.reset ();

 	     "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",

 CalcTree @{context} [(fmz, (dI',pI',mI'))];

 	     "AbleitungBiegelinie dy"];

 Iterator 1;

 val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"],

 moveActiveRoot 1;

 		     ["IntegrierenUndKonstanteBestimmen2"]);

 autoCalculate 1 CompleteCalc;

 val ((pt, p),_) = States.get_calc 1;

 (* ERROR: THIS TEST WAS BROKEN BEFORE CS "eliminate ThmC.numerals_to_Free", 

    UNDETECTED BY Test_Isac_Short.thy ===========================================================\\

 if p = ([], Res) andalso (get_obj g_res pt (fst p) |> UnparseC.term @{context}) =

    "[Q x = c + - 1 * q_0 * x, M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n dy x =\n c_3 + 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n y x =\n c_4 + c_3 * x +\n 1 / (- 1 * EI) *\n (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]"

 then () else error "auto SubProblem (_,[vonBelastungZu,Biegelinien] changed";

 ===============================================================================================//*)

 \<close> ML \<open>

 "----------- me SubProblem (_,[vonBelastungZu,Biegelinien] -------";

 "----------- me SubProblem (_,[vonBelastungZu,Biegelinien] -------";

 "----------- me SubProblem (_,[vonBelastungZu,Biegelinien] -------";

 val fmz = 

     ["Streckenlast q_0", "FunktionsVariable x",

      "Funktionen [Q x = c + - 1 * q_0 * x, \

      \M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\

      \ y' x = c_3 + 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\

      \ y x = c_4 + c_3 * x + 1 / (- 1 * EI) * (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]",

     "AbleitungBiegelinie dy"];

 val (dI',pI',mI') = ("Biegelinie", ["vonBelastungZu", "Biegelinien"],

 		     ["Biegelinien", "ausBelastung"]);

 (*[], Pbl*)val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))]; val Model_Problem = nxt

 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))]; val Model_Problem = nxt

 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Traegerlaenge L" = nxt

 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Streckenlast q_0" = nxt

 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Streckenlast q_0" = nxt

 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "FunktionsVariable x" = nxt

 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "Biegelinie y" = nxt

 \<close> ML \<open> (*isa*) 

 \<close> ML \<open>

 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "Funktionen\n [Q x = c + - 1 * q_0 * x, M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n  y' x =\n  c_3 +\n  1 / (- 1 * EI) *\n  (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n  y x =\n  c_4 + c_3 * x +\n  1 / (- 1 * EI) *\n  (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]" = nxt

 (*/---broken elementwise input to lists---\* )

 \<close> text \<open> (*isa2* )

 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Relation "Randbedingungen [y 0 = 0]", ERROR MISSING step: M_b 0 = 0*)

 (*/---broken elementwise input to lists---\*)

                                         (*isa* ) val Add_Relation "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]" = nxt

 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "Funktionen [Q x = c + - 1 * q_0 * x]" = nxt

                                         ( *isa2*) val Add_Relation "Randbedingungen [y 0 = 0]" = nxt

 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "Funktionen\n [M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n  y' x =\n  c_3 +\n  1 / (- 1 * EI) *\n  (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n  y x =\n  c_4 + c_3 * x +\n  1 / (- 1 * EI) *\n  (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]" = nxt

 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Relation "Randbedingungen [y L = 0, M_b 0 = 0, M_b L = 0]"*)

                                         (*isa*) val Specify_Theory "Biegelinie" = nxt

                                         (*isa2* ) val Add_Relation "Randbedingungen [y L = 0, M_b 0 = 0, M_b L = 0]" = nxt( **)

 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]" = nxt

 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Theory "Biegelinie" = nxt

 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Theory "Biegelinie" = nxt

 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["vonBelastungZu", "Biegelinien"] = nxt

 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["Biegelinien"] = nxt

 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["Biegelinien", "ausBelastung"] = nxt

 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt

 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "AbleitungBiegelinie dy" = nxt

 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "FunktionsVariable x" = nxt

 \<close> text \<open> (*ERROR in creating the environment from formal args*)

 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "GleichungsVariablen [c, c_2, c_3, c_4]" = nxt

 val return_me_Add_Given_AbleitungBiegelinie

 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "AbleitungBiegelinie dy" = nxt

                      = me nxt p c pt;

 \<close> ML \<open> (*//----------- step into me_Add_Given_AbleitungBiegelinie --------------------------\\*)

 \<close> text \<open> (*ERROR type_of: real/real list/(#) [c_4]*)

 (*//------------------ step into me_Add_Given_AbleitungBiegelinie --------------------------\\*)

 (*[], Met*)val return_Add_Given_AbleitungBieg

 \<close> ML \<open>

                                 = me nxt p c pt;

 \<close> ML \<open> (*/------------ step into me_Add_Given_AbleitungBieg --------------------------------\\*)

 (*/------------------- step into me_Add_Given_AbleitungBieg --------------------------------\\*)

 val ("ok", (_, _, ptp as (pt, p))) =

       val (pt, p) = 

   	    (*case*) Step.by_tactic tac (pt, p) (*of*);

   	    (*Step.by_tactic is here for testing by me; do_next would suffice in me*)

   	    case Step.by_tactic tac (pt, p) of

 \<close> text \<open> (*ERROR type_of: real/real list/(#) [c_4]*)

   		    ("ok", (_, _, ptp)) => ptp

         (*case*)

 \<close> text \<open> (*ERROR in creating the environment from formal args*)

     (*case*)

   (p, ((pt, Pos.e_pos'), []) );

   (p, ((pt, Pos.e_pos'), []));

 \<close> ML \<open>

   (*if*) Pos.on_calc_end ip (*else*);

 \<close> ML \<open>

       val (_, probl_id, _) = Calc.references (pt, p);

 \<close> ML \<open>

 val _ =

       (*case*) tacis (*of*);

 \<close> ML \<open>

         (*if*) probl_id = Problem.id_empty (*else*);

 \<close> text \<open> (*ERROR in creating the environment from formal args*)

            switch_specify_solve p_ (pt, ip);

 \<close> ML \<open>

 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));

 \<close> ML \<open>

       (*if*) Pos.on_specification ([], state_pos) (*then*);

 \<close> text \<open> (*ERROR in creating the environment from formal args*)

            specify_do_next (pt, input_pos);

 \<close> ML \<open>

 "~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);

 \<close> ML \<open>

     val (_, (p_', tac)) = Specify.find_next_step ptp

     val ist_ctxt =  Ctree.get_loc pt (p, p_)

 \<close> ML \<open>

 val Tactic.Apply_Method mI =

     (*case*) tac (*of*);

 \<close> text \<open> (*ERROR in creating the environment from formal args*)

   	    LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty))

   	      ist_ctxt (pt, (p, p_'));

 \<close> ML \<open>

 "~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _))) =

   ((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)), ist_ctxt, (pt, (p, p_')));

 \<close> ML \<open>

       val (itms, oris, probl) = case get_obj I pt p of

           PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)

         | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj"

       val {model, ...} = MethodC.from_store ctxt mI;

 \<close> ML \<open>

 (*+*)val "Biegelinien/ausBelastung" = mI |> References.implode_id

 \<close> ML \<open>

 (*+* ===== current MethodC i_model ==============================================================*)

 (*+*)if (itms |> I_Model.to_string @{context}) = "[\n" ^

   "(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^

   "(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])), \n" ^

   "(3 ,[1] ,true ,#Find ,Cor Funktionen\n [Q x = c + - 1 * q_0 * x, M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n  y' x =\n  c_3 +\n  1 / (- 1 * EI) *\n  (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n  y x =\n  c_4 + c_3 * x +\n  1 / (- 1 * EI) *\n  (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)] ,(funs''', [[Q x = c + - 1 * q_0 * x, M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n y' x =\n c_3 +\n 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n y x =\n c_4 + c_3 * x +\n 1 / (- 1 * EI) *\n (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]])), \n" ^

 (*  ...................... Cor Biegemoment M_b,

     ...................... Cor Querkraft Q    , *)

   "(4 ,[1] ,true ,#Given ,Cor AbleitungBiegelinie dy ,(id_der, [dy]))]"

 (* ...................... Cor Biegelinie y    , *)

 then () else error "by_tactic: parent "

 \<close> ML \<open>

 (*+* ===== current o_model created from Formalise.model of SubProblem ===========================*)

 (*+*)(oris |> O_Model.to_string @{context}) = "[\n" ^

   "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^

   "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^

   "(3, [\"1\"], #Find, Funktionen, [\"[Q x = c + - 1 * q_0 * x]\", \"[M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2]\", \"[y' x =\n c_3 +\n 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3)]\", \"[y x =\n c_4 + c_3 * x +\n 1 / (- 1 * EI) *\n (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]\"]), \n" ^

   "(4, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]"

 \<close> ML \<open>

 (*+* ===== parent Problem i_model ===============================================================*)

 (*+*)(probl |> I_Model.to_string @{context}) = "[\n" ^

   "(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^

   "(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])), \n" ^

   "(3 ,[1] ,true ,#Find ,Cor Funktionen\n [Q x = c + - 1 * q_0 * x, M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n  y' x =\n  c_3 +\n  1 / (- 1 * EI) *\n  (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n  y x =\n  c_4 + c_3 * x +\n  1 / (- 1 * EI) *\n  (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)] ,(funs''', [[Q x = c + - 1 * q_0 * x, M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n y' x =\n c_3 +\n 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n y x =\n c_4 + c_3 * x +\n 1 / (- 1 * EI) *\n (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]]))]"

 \<close> ML \<open>

       val itms = if itms <> [] then itms else I_Model.complete oris probl [] model

 \<close> ML \<open>

 (*+* ===== current MethodC i_model complete'd ===================================================*)

 (*+*)(itms |> I_Model.to_string @{context}) = "[\n" ^

   "(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^

   "(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])), \n" ^

   "(3 ,[1] ,true ,#Find ,Cor Funktionen\n [Q x = c + - 1 * q_0 * x, M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n  y' x =\n  c_3 +\n  1 / (- 1 * EI) *\n  (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n  y x =\n  c_4 + c_3 * x +\n  1 / (- 1 * EI) *\n  (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)] ,(funs''', [[Q x = c + - 1 * q_0 * x, M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n y' x =\n c_3 +\n 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n y x =\n c_4 + c_3 * x +\n 1 / (- 1 * EI) *\n (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]])), \n" ^

   "(4 ,[1] ,true ,#Given ,Cor AbleitungBiegelinie dy ,(id_der, [dy]))]"

 \<close> ML \<open>

 \<close> text \<open> (*ERROR in creating the environment from formal args*)

       val (is, env, ctxt, prog) = case

     LItool.init_pstate ctxt (I_Model.OLD_to_TEST itms) mI of

           (is as Pstate {env, ...}, ctxt, program) => (is, env, ctxt, program)

 \<close> ML \<open>

 "~~~~~ fun init_pstate , args:"; val (ctxt, i_model, met_id) = (ctxt, (I_Model.OLD_to_TEST itms), mI);

 \<close> ML \<open>

     val (model_patt, program, prog, prog_rls, where_, where_rls) =

       case MethodC.from_store ctxt met_id of

         {model = model_patt, program = program as Rule.Prog prog, prog_rls, where_, where_rls,...}=>

           (model_patt, program, prog, prog_rls, where_, where_rls)

 \<close> ML \<open>

 (*+* ===== MethodC model_patt ===================================================================*)

 (*+*)if (model_patt |> Model_Pattern.to_string @{context}) = "[\"" ^

   (*5 elements ------------------------------------------ ERROR:  -------------CORRECT:          *)

   "(#Given, (Streckenlast, q__q))\", \"" ^

   "(#Given, (FunktionsVariable, v_v))\", \"" ^

   "(#Given, (Biegelinie, b_b))\", \"" ^             (*\<longrightarrow> (b_b, dy)            (b_b, y)          *)

   "(#Given, (AbleitungBiegelinie, id_der))\", \"" ^ (*\<longrightarrow> (id_der, [Q x =..])  (id_der, dy)      *)

   "(#Find, (Funktionen, fun_s))\"]"                 (*                         (fun_s, [Q x =..])*)

 then () else error "init_pstate initial model_patt CHANGED"

 \<close> ML \<open>

 (*+*)if (i_model |> I_Model.to_string_TEST @{context}) = "[\n" ^

   "(1, [1], true ,#Given, (Cor_TEST Streckenlast q_0 , pen2str, Position.T)), \n" ^

   "(2, [1], true ,#Given, (Cor_TEST FunktionsVariable x , pen2str, Position.T)), \n" ^

   "(3, [1], true ,#Find, (Cor_TEST Funktionen\n [" ^

     "Q x = c + - 1 * q_0 * x, " ^

     "M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n  " ^

     "y' x =\n  c_3 +\n  1 / (- 1 * EI) *\n  (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n  " ^

     "y x =\n  c_4 + c_3 * x +\n  1 / (- 1 * EI) *\n  (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)] , pen2str, Position.T)), \n" ^

   "(4, [1], true ,#Given, (Cor_TEST AbleitungBiegelinie dy , pen2str, Position.T))]"

 (*MISSING: ------------------------------------------------------------------- (b_b, y)          *)

 then () else error "init_pstate initial i_model CHANGED";

 \<close> ML \<open> (*isa*)

     val (_, env_model, (env_subst, env_eval)) = I_Model.of_max_variant model_patt i_model;

 (*?! complete with Met.i_model ?!*)

 \<close> ML \<open> (*isa*)

 (*+*)if (env_model |> Subst.to_string @{context}) = "[\"\n" ^

   "(q__q, q_0)\", \"\n" ^

   "(v_v, x)\", \"\n" ^

   "(id_der, dy)\", \"\n" ^

   "(fun_s, [Q x = c + - 1 * q_0 * x, M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n y' x =\n c_3 +\n 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n y x =\n c_4 + c_3 * x +\n 1 / (- 1 * EI) *\n (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)])\"]"

 then () else error "init_pstate: env_model CHANGED";

 \<close> ML \<open> (*isa*)

     val actuals = map snd env_model

 \<close> text \<open> (*isa2*)

     val (_, env_subst, env_eval) = I_Model.of_max_variant model_patt i_model;

     val actuals = map snd env_subst

 \<close> ML \<open> (*isa==isa2*)

 (*+*)val "[q_0, x, dy, [Q x = c + - 1 * q_0 * x, M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n y' x =\n c_3 +\n 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n y x =\n c_4 + c_3 * x +\n 1 / (- 1 * EI) *\n (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]]"

  = actuals |> UnparseC.terms @{context}

 \<close> ML \<open> (*isa==isa2*)

     val formals = Program.formal_args prog    

 \<close> ML \<open> (*isa==isa2*)

 (*+*)val "[q__q, v_v, b_b, id_der]" = formals |> UnparseC.terms @{context} (*From fun. belastung_zu_biegelinie*)

 \<close> ML \<open> (*isa*)

     val preconds = Pre_Conds.check_envs_TEST ctxt where_rls where_ (env_model, (env_subst, env_eval))

     val ctxt = ctxt |> ContextC.insert_assumptions (map snd (snd preconds));

 \<close> text \<open> (*ERROR in creating the environment from formal args*)

     val ist = Istate.e_pstate

       |> Istate.set_eval prog_rls

       |> Istate.set_env_true (relate_args [] formals actuals ctxt prog met_id formals actuals)

 \<close> text \<open> (*ERROR in creating the environment from formal args*)

           (relate_args [] formals actuals ctxt prog met_id formals actuals);

 \<close> ML \<open>

 "~~~~~ fun relate_args , args:"; val (env, (f::ff), (aas as (a::aa)), ctxt, prog, met_id, formals, actuals) =

   ([], formals, actuals, ctxt, prog, met_id, formals, actuals);

     (*if*) type_of f = type_of a (*then*);

 \<close> text \<open> (*ERROR in creating the environment from formal args*)

            relate_args (env @ [(f, a)]) ff aa ctxt prog met_id formals actuals;

 \<close> ML \<open>

 (*+*)val "q__q" = f |> UnparseC.term @{context}

 (*+*)val "q_0" = a |> UnparseC.term @{context};

 \<close> ML \<open>

     (*if*) type_of f = type_of a (*then*);

 \<close> text \<open> (*ERROR in creating the environment from formal args*)

            relate_args (env @ [(f, a)]) ff aa ctxt prog met_id formals actuals;

 \<close> ML \<open>

 "~~~~~ fun relate_args , args:"; val (env, (f::ff), (aas as (a::aa)), ctxt, prog, met_id, formals, actuals) =

   ((env @ [(f, a)]), ff, aa, ctxt, prog, met_id, formals, actuals)

 \<close> ML \<open>

 (*+*)val "v_v" = f |> UnparseC.term @{context}

 (*+*)val "x" = a |> UnparseC.term @{context}

 \<close> ML \<open>

     (*if*) type_of f = type_of a (*then*);

 \<close> text \<open> (*ERROR in creating the environment from formal args*)

            relate_args (env @ [(f, a)]) ff aa ctxt prog met_id formals actuals;

 \<close> ML \<open>

 "~~~~~ fun relate_args , args:"; val (env, (f::ff), (aas as (a::aa)), ctxt, prog, met_id, formals, actuals) =

   ((env @ [(f, a)]), ff, aa, ctxt, prog, met_id, formals, actuals)

 \<close> ML \<open>

 (*+*)val "b_b" = f |> UnparseC.term @{context} (*ERROR: IS Biegelinie*)

 (*+*)val "dy" = a |> UnparseC.term @{context}  (*ERROR: IS AbleitungBiegelinie*)

 (*CONCLUSION: if the type is equal, then the sequence decides the pairing for env

   (q__q, q_0)

   (v_v, x)

 *)

 \<close> ML \<open>

     (*if*) type_of f = type_of a (*then*);

 \<close> ML \<open>

 \<close> text \<open> (*ERROR in creating the environment from formal args*)

            relate_args (env @ [(f, a)]) ff aa ctxt prog met_id formals actuals;

 \<close> ML \<open>

 "~~~~~ fun relate_args , args:"; val (env, (f::ff), (aas as (a::aa)), ctxt, prog, met_id, formals, actuals) =

   ((env @ [(f, a)]), ff, aa, ctxt, prog, met_id, formals, actuals)

 \<close> ML \<open>

 (*+*)val "id_der" = f |> UnparseC.term @{context} (*ERROR IS AbleitungBiegelinie*)

 (*+*)val "[Q x = c + - 1 * q_0 * x, M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n y' x =\n c_3 +\n 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n y x =\n c_4 + c_3 * x +\n 1 / (- 1 * EI) *\n (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]"

  = a |> UnparseC.term @{context}                  (*ERROR IS FROM Pbl.i_model*)

 \<close> ML \<open>

     (*if*) type_of f = type_of a (*else*);

 \<close> text \<open> (*ERROR in creating the environment from formal args*)

         val (f, a) =

            assoc_by_type ctxt f aas prog met_id formals actuals;

 \<close> ML \<open>

 "~~~~~ fun assoc_by_type , args:"; val (ctxt, f, aa, prog, met_id, formals, actuals) =

   (ctxt, f, aas, prog, met_id, formals, actuals);

 \<close> ML \<open>

 val [] =

   (*case*) filter (curry (fn (f, a) => type_of f = type_of a) f) aa (*of*);

 \<close> ML \<open>

 (*+*)val Free ("id_der", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])) = f

 \<close> ML \<open>

 (*+*)val [Const ("List.list.Cons", _) $ _ $

       (Const ("List.list.Cons", _) $ _ $

         (Const ("List.list.Cons", _) $ _ $

           (Const ("List.list.Cons", _) $ _ $

             Const ("List.list.Nil", list_elem_type))))] = aa

 (*+*)val Type ("List.list", [Type ("HOL.bool", [])]) = list_elem_type

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open> (*||----------- continuing me_Add_Given_AbleitungBiegelinie ---------------------------*)

 (*||------------------ continuing me_Add_Given_AbleitungBiegelinie ---------------------------*)

 (*\\------------------ step into XXXXX -----------------------------------------------------//*)

 \<close> ML \<open> (*\\----------- step into XXXXX -----------------------------------------------------//*)

 \<close> text \<open> (*ERROR in creating the environment from formal args*)

 val (p,_,f,nxt,_,pt) = return_me_Add_Given_AbleitungBiegelinie;

 \<close> ML \<open>

 (*ERROR arguments_from_model: 'Biegelinie' not in itms: ...(**)

 val (p,_,f,nxt,_,pt) = me nxt p c pt;

 *)

 (* ERROR: THIS TEST WAS BROKEN BEFORE CS "eliminate ThmC.numerals_to_Free", 

    UNDETECTED BY Test_Isac_Short.thy

 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

 arguments_from_model: 'Biegelinie' not in itms:

 itms:

 [

 (1 ,[1] ,true ,#Given ,Cor ??.Biegelinie.Streckenlast q_0 ,(q_q, [q_0])), 

 (2 ,[1] ,true ,#Given ,Cor ??.Biegelinie.FunktionsVariable x ,(v_v, [x])), 

 (3 ,[1] ,true ,#Find ,Cor ??.Biegelinie.Funktionen [

   ??.Biegelinie.Q x = c + - 1 * q_0 * x,

   ??.Biegelinie.M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,

   ??.Biegelinie.y' x = c_3 + 1 / (- 1 * ??.Biegelinie.EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),

   y x = c_4 + c_3 * x + 1 / (- 1 * ??.Biegelinie.EI) * (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)],

  (funs''', [[

   ??.Biegelinie.Q x = c + - 1 * q_0 * x,

   ??.Biegelinie.M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,

   ??.Biegelinie.y' x = c_3 + 1 / (- 1 * ??.Biegelinie.EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),

   y x = c_4 + c_3 * x + 1 / (- 1 * ??.Biegelinie.EI) * (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]]) ), 

 (4 ,[1] ,true ,#Given ,Cor ??.Biegelinie.AbleitungBiegelinie dy ,(id_der, [dy]))]

 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

 CORRECTION:

 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

 Const ("Biegelinie.Biegelinie", _) MUST BE IN itms OF THE model,

 BECAUSE REQUIRED BY GUARD OF MethodC.

 *)

 (*//---------------- adhoc inserted ------------------------------------------------\\*)

 \<close> ML \<open>

 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);

       val (pt, p) = 

   	    (*Step.by_tactic is here for testing by me; do_next would suffice in me*)

   	    case Step.by_tactic tac (pt, p) of

   		    ("ok", (_, _, ptp)) => ptp

   	    | ("unsafe-ok", (_, _, ptp)) => ptp

   	    | ("not-applicable",_) => (pt, p)

   	    | ("end-of-calculation", (_, _, ptp)) => ptp

   	    | ("failure", _) => raise ERROR "sys-raise ERROR by Step.by_tactic"

   	    | _ => raise ERROR "me: uncovered case Step.by_tactic";

 \<close> ML \<open>

 (*ERROR arguments_from_model: 'Biegelinie' not in itms: ...(**)

   	     (*case*) 

       Step.do_next p ((pt, Pos.e_pos'), []) (*of*);

 *)

 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =

   (p, ((pt, Pos.e_pos'), []));

 \<close> text \<open> (*ERROR type_of: real/real list/(#) [c_4]*)

 (*ERROR arguments_from_model: 'Biegelinie' not in itms: ...(**)

            switch_specify_solve p_ (pt, ip);

            switch_specify_solve p_ (pt, ip)

 \<close> ML \<open>

 *)

        (*if*) Pos.on_specification ([], state_pos) (*then*);

       (*if*) Pos.on_specification ([], state_pos) (*then*);

 \<close> text \<open> (*ERROR type_of: real/real list/(#) [c_4]*)

 (*ERROR arguments_from_model: 'Biegelinie' not in itms: ...(**)

            specify_do_next (pt, input_pos);

            specify_do_next (pt, input_pos)

 \<close> ML \<open>

 *)

 \<close> text \<open> (*ERROR type_of: real/real list/(#) [c_4]*)

 (*ERROR arguments_from_model: 'Biegelinie' not in itms: ...(**)

   	    LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty))

   	    LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)) ist_ctxt (pt, (p, p_'))

   	      ist_ctxt (pt, (p, p_'));

 *)

 \<close> ML \<open>

   ((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)), ist_ctxt, (pt, (p, p_')));

 ((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)), ist_ctxt, (pt, (p, p_')));

       val (itms, oris, probl) = case get_obj I pt p of (*STILL asms=[]*)

          val (itms, (*l..*)oris, probl(*..l*)) = case get_obj I pt p of

           PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)

            PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)

         | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj"

          | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj"

       val {model, ...} = MethodC.from_store ctxt mI;

          val {model, ...} = MethodC.from_store ctxt mI;

       val itms = if itms <> [] then itms else I_Model.complete oris probl [] model

          val itms = if itms <> [] then itms else I_Model.complete oris probl [] model

 ;

          val prog_rls = LItool.get_simplifier (pt, pos);

 (*+*)if (itms |> I_Model.to_string @{context}) = "[\n" ^

   "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L ,(l_l, [L])), \n" ^

 (*ERROR arguments_from_model: 'Biegelinie' not in itms: ...(**)

   "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^

           (*case*) 

   "(3 ,[1] ,true ,#Find ,Cor Biegelinie y ,(b_b, [y])), \n" ^

     LItool.init_pstate prog_rls ctxt itms mI (*of*);

   "(4 ,[1] ,true ,#Relate ,Cor Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] ,(r_b, [[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]])), \n" ^

 *)

   "(5 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(fun_var, [x])), \n" ^

 "~~~~~ fun init_pstate , args:"; val (prog_rls, ctxt, itms, metID) = (prog_rls, ctxt, itms, mI);

   "(6 ,[1] ,true ,#Given ,Cor GleichungsVariablen [c, c_2, c_3, c_4] ,(vs, [[c, c_2, c_3, c_4]])), \n" ^

 (*ERROR arguments_from_model: 'Biegelinie' not in itms: ... (**)

   "(7 ,[1] ,true ,#Given ,Cor AbleitungBiegelinie dy ,(id_der, [dy]))]"

     val actuals = 

 (*+*)then () else error "init_pstate: initial i_model changed";

            arguments_from_model metID itms

 (*+*)if (itms |> I_Model.penv_to_string @{context}) = "[" ^ (*to be eliminated*)

 *)

 (*1*)"(l_l, [L]), " ^

 \<close> ML \<open>

 (*2*)"(q_q, [q_0]), " ^

 "~~~~~ fun arguments_from_model , args:"; val (mI, itms) = (metID, itms);

 (*3*)"(b_b, [y]), " ^

     val mvat = Pre_Conds.max_variant itms

 (*4*)"(r_b, [[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]]), " ^

     fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b

 (*5*)"(fun_var, [x]), " ^

     val itms = filter (okv mvat) itms;

 (*6*)"(vs, [[c, c_2, c_3, c_4]]), " ^

 (*7*)"(id_der, [dy])]"

 I_Model.to_string @{context} itms |> writeln;

 (*+*)then () else error "init_pstate: initial penv changed";

 (*[

 (1 ,[1] ,true ,#Given ,Cor ??.Biegelinie.Streckenlast q_0 ,(q_q, [q_0])), 

 \<close> text \<open> (*ERROR type_of: real/real list/(#) [c_4]*)

 (2 ,[1] ,true ,#Given ,Cor ??.Biegelinie.FunktionsVariable x ,(v_v, [x])), 

     (*case*)

 (3 ,[1] ,true ,#Find ,Cor ??.Biegelinie.Funktionen [

     LItool.init_pstate ctxt (I_Model.OLD_to_TEST itms) mI (*of*);

   ??.Biegelinie.Q x = c + - 1 * q_0 * x,

 \<close> ML \<open>(*//------------ step into init_pstate -----------------------------------------------\\*)

   ??.Biegelinie.M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,

 (*//------------------ step into init_pstate -----------------------------------------------\\*)

   ??.Biegelinie.y' x = c_3 + 1 / (- 1 * ??.Biegelinie.EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),

 "~~~~~ fun init_pstate , args:"; val (ctxt, i_model, met_id) = (ctxt, (I_Model.OLD_to_TEST itms), mI);

   y x = c_4 + c_3 * x + 1 / (- 1 * ??.Biegelinie.EI) * (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)],

     val (model_patt, program, prog, prog_rls, where_, where_rls) =

  (funs''', [[

       case MethodC.from_store ctxt met_id of

   ??.Biegelinie.Q x = c + - 1 * q_0 * x,

         {model = model_patt, program = program as Rule.Prog prog, prog_rls, where_, where_rls,...}=>

   ??.Biegelinie.M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,

           (model_patt, program, prog, prog_rls, where_, where_rls)

   ??.Biegelinie.y' x = c_3 + 1 / (- 1 * ??.Biegelinie.EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),

   y x = c_4 + c_3 * x + 1 / (- 1 * ??.Biegelinie.EI) * (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]]) ), 

 \<close> ML \<open>

 (4 ,[1] ,true ,#Given ,Cor ??.Biegelinie.AbleitungBiegelinie dy ,(id_der, [dy]))]

     val return_of_max_variant = 

 *)

    I_Model.of_max_variant model_patt i_model;

     fun test_dsc d (_, _, _, _, itm_) = (d = I_Model.descriptor itm_)

 \<close> ML \<open>(*///----------- step into of_max_variant --------------------------------------------\\*)

     fun itm2arg itms (_, (d, _)) =

 (*///----------------- step into of_max_variant --------------------------------------------\\*)

       case find_first (test_dsc d) itms of

 "~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) = (model_patt, i_model);

         NONE => raise ERROR "arguments_from_model ..."(*error_msg_2 d itms*)

     val all_variants =

       | SOME (_, _, _, _, itm_) => I_Model.penvval_in itm_

         map (fn (_, variants, _, _, _) => variants) i_model

         |> flat

     val pats = (#model o MethodC.from_store ctxt) mI;

         |> distinct op =

 (*[("#Given", (Const ("Biegelinie.Streckenlast", "real \<Rightarrow> una"), Free ("q__q", "real"))), 

     val variants_separated = map (filter_variants' i_model) all_variants

     ("#Given", (Const ("Biegelinie.FunktionsVariable", "real \<Rightarrow> una"), Free ("v_v", "real"))),

     val sums_corr = map (cnt_corrects) variants_separated

     ("#Given", (Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), Free ("b_b", "real \<Rightarrow> real"))),

     val sum_variant_s = arrange_args1 sums_corr (1, all_variants)

     ("#Given", (Const ("Biegelinie.AbleitungBiegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), Free ("id_der", "real \<Rightarrow> real"))),

     val (_, max_variant) = hd (*..crude decision, up to improvement *)

     ("#Find", (Const ("Biegelinie.Funktionen", "bool list \<Rightarrow> una"), Free ("fun_s", "bool list")))]:

       (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)

    Model_Pattern.T*)

     val i_model_max =

 (*ERROR arguments_from_model: 'Biegelinie' not in itms: ... (**)

       filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model

        (flat o (map (

     val equal_descr_pairs = map (get_equal_descr i_model) model_patt |> flat

            itm2arg itms))) pats

 ;

 *)

 (*+*)if (equal_descr_pairs |> descr_pairs_to_string @{context}) = "[" ^

 "~~~~~ fun itm2arg , args:"; val (itms, (_, (d, _))) = (itms, nth 1 pats);

 (*defined: in program+model--vvvv--,----------------------------------------- in problem ---vvv*)

 val SOME (1, [1], true, "#Given", Cor ((Const ("Biegelinie.Streckenlast", _), [Free ("q_0", _)]), (Free ("q_q", _), [Free ("q_0", _)]))) =

   "((#Given, (Traegerlaenge, l_l)), (1, [1], true ,#Given, " ^ "(Cor_TEST Traegerlaenge L ,(l_l, [L]), Position.T))), " ^

         find_first (test_dsc d) itms;

   "((#Given, (Streckenlast, q_q)), (2, [1], true ,#Given, " ^

    "(Cor_TEST Streckenlast q_0 ,(q_q, [q_0]), Position.T))), " ^

 "~~~~~ fun itm2arg , args:"; val (itms, (_, (d, _))) = (itms, nth 2 pats);

   "((#Given, (FunktionsVariable, fun_var)), (5, [1], true ,#Given, " ^

 val SOME (2, [1], true, "#Given", Cor ((Const ("Biegelinie.FunktionsVariable", _), [Free ("x", _)]), (Free ("v_v", _), [Free ("x", _)]))) =

    "(Cor_TEST FunktionsVariable x ,(fun_var, [x]), Position.T))), " ^

         find_first (test_dsc d) itms;

   "((#Given, (GleichungsVariablen, vs)), (6, [1], true ,#Given, " ^

    "(Cor_TEST GleichungsVariablen [c, c_2, c_3, c_4] ,(vs, [[c, c_2, c_3, c_4]]), Position.T))), " ^

 "~~~~~ fun itm2arg , args:"; val (itms, (_, (d, _))) = (itms, nth 3 pats);

   "((#Given, (AbleitungBiegelinie, id_der)), (7, [1], true ,#Given, " ^

 val Const ("Biegelinie.Biegelinie", _) = d

    "(Cor_TEST AbleitungBiegelinie dy ,(id_der, [dy]), Position.T))), " ^

 val NONE =

   "((#Find, (Biegelinie, b_b)), (3, [1], true ,#Find, (Cor_TEST Biegelinie y ,(b_b, [y]), Position.T))), " ^

         find_first (test_dsc d) itms;

   "((#Relate, (Randbedingungen, r_b)), (4, [1], true ,#Relate, " ^

    "(Cor_TEST Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] ,(r_b, [[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]]), Position.T)))]"

 "~~~~~ fun itm2arg , args:"; val (itms, (_, (d, _))) = (itms, nth 4 pats);

 then () else error "of_max_variant: equal_descr_pairs CHANGED";

 val SOME (4, [1], true, "#Given", Cor ((Const ("Biegelinie.AbleitungBiegelinie", _), [Free ("dy", _)]), (Free ("id_der", _), [Free ("dy", _)]))) =

 (*/////############### old test code ##################################################\\\\\\* )

         find_first (test_dsc d) itms;

     val env_subst =

 "~~~~~ fun itm2arg , args:"; val (itms, (_, (d, _))) = (itms, nth 5 pats);

            mk_env_subst_DEL equal_descr_pairs;

 val SOME (3, [1], true, "#Find", Cor ((Const ("Biegelinie.Funktionen", _), _), (Free ("funs'''", _), _))) =

 (*/------------------- ERRORs to remove in CS subsequent to "prepare 1 PIDE turn 11"-000----\* )

         find_first (test_dsc d) itms

 (*+*)if (     env_subst |> Subst.to_string @{context}) = "[\"\n" ^

 (*ERRORs------^^^^^^^^^----------isa2: penv ---vvv----------------------..isa2, thus "correct"*)         

 (*\\---------------- adhoc inserted ------------------------------------------------//*)

 (*1*)"(l_l, L)\", \"\n" ^                  (* (l_l, [L]) *)

 \<close> ML \<open>

 (*2*)"(q_q, q_0)\", \"\n" ^                (* (q_q, [q_0]) *)

 (* ERROR: THIS TEST WAS BROKEN BEFORE CS "eliminate ThmC.numerals_to_Free", 

 (*3*)"(fun_var, x)\", \"\n" ^              (* (fun_var, [x]) *)

    UNDETECTED BY Test_Isac_Short.thy ===========================================================\\

 (*4*)"(vs, GleichungsVariablen)\", \"\n" ^ (* (vs, [[c, c_2, c_3, c_4]]) *)

 case nxt of ("Apply_Method", Apply_Method ["Biegelinien", "ausBelastung"]) => ()

 (*5*)"(id_der, dy)\", \"\n" ^              (* (id_der, [dy]) *)

 | _ => error "biegelinie.sml met2 b";

 (*6*)"(b_b, y)\"]"                         (* (b_b, [y]) *)

 (*7 missing*)                              (* (r_b, [[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]]) *)

 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =   "q_ x = q_0";

 (*+*)then () else error "of_max_variant: env_subst BETTER ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? "

 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "- q_ x = - q_0";

 ( *\------------------- ERRORs to remove ..--------------------------------------------------/*)

 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =  "Q' x = - q_0";

 case nxt of (_, Subproblem (_, ["named", "integrate", "function"])) => ()

 (*///----------------- step into mk_env_subst_DEL ------------------------------------------\\*)

 | _ => error "biegelinie.sml met2 c";

 "~~~~~ fun mk_env_subst_DEL , args:"; val (equal_descr_pairs) = (equal_descr_pairs);

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 (*///################# nth 1 equal_descr_pairs ############################################=\\*)

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

        val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

         => (Pre_Conds.discern_feedback_subst id feedb) (*|> map fst (*rhs dropped*)|> map (pair id)*) ) (nth 1 equal_descr_pairs);

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 "~~~~~ fun xxx , args:"; val ((_, (_, id)), (_, _, _, _, (feedb, _))) = (nth 1 equal_descr_pairs);

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 (*--------------------------------------------------------------------------^^^----------------*)

 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q x = c + - 1 * q_0 * x";

  Pre_Conds.discern_feedback_subst id feedb;

 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q x = c + - 1 * q_0 * x";

 "~~~~~ fun discern_feedback_subst , args:"; val (id, Cor_TEST ((descr, [ts]), _)) = (id, feedb);

 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "M_b' x = c + - 1 * q_0 * x";

       (*if*) TermC.is_list ts (*else*);

 case nxt of (_,Subproblem (_, ["named", "integrate", "function"])) => ()

       val ts = [ts]

 | _ => error "biegelinie.sml met2 d";

 ;

  Pre_Conds.discern_type_subst (descr, id) ts;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 "~~~~~ fun discern_type_subst , args:"; val ((descr, id), ts) = ((descr, id), ts);

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val _(*"real \<Rightarrow> una"*) =

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

   (*case*) type_of descr (*of*);

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val return_discern_type_subst_1 = [(id, Library.the_single ts)]

 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = 

 (*\\\################# nth 1 equal_descr_pairs ############################################=//*)

 		   "M_b x = Integral c + - 1 * q_0 * x D x";

 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = 

 (*///################# nth 4 equal_descr_pairs ############################################=\\*)

 		   "M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2";

        val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))

 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =

         => (discern_feedback_subst id feedb) (*|> map fst (*rhs dropped*)|> map (pair id)*) ) (nth 1 equal_descr_pairs);

 		   "M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2";

 "~~~~~ fun xxx , args:"; val ((_, (_, id)), (_, _, _, _, (feedb, _))) = (nth 4 equal_descr_pairs);

 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =

 (*--------------------------------------------------------------------------^^^----------------*)

 		   "- EI * y'' x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2";

 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =

  Pre_Conds.discern_feedback_subst id feedb;

 		   "y'' x = 1 / - EI * (c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2)";

 "~~~~~ fun discern_feedback_subst , args:"; val (id, Cor_TEST ((descr, (*[*)ts(*]*)), _)) = (id, feedb);

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 (*+*)val (Free ("vs", _), "[[c], [c_2], [c_3], [c_4]]")

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

   = (id, ts |> UnparseC.terms @{context});

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

     (*if*) fold (curry and_) (map TermC.is_list ts) true (*then*);

 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =

       val ts = ts;

     "y' x = Integral 1 / - EI * (c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2) D x";

 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =

            discern_type_subst (descr, id) ts;

 "y' x = Integral 1 / (- 1 * EI) * (c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2) D x";

 "~~~~~ fun discern_type_subst , args:"; val ((descr, id), ts) = ((descr, id), ts);

 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =

 val (Type ("fun", [Type ("List.list", [Type ("Real.real", [])]), _])) =

 "y' x =\nc_3 + 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3)";

   (*case*) type_of descr (*of*);

 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =

          (*if*) TermC.is_list (hd ts) (*then*);

 "y' x =\nc_3 + 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3)";

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val return_discern_type_subst_4 =

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 (*       if TermC.is_list (hd ts)

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

          then*) [(id, ts |> map TermC.the_single |> TermC.list2isalist HOLogic.realT)]

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 (*       else []*)

 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =

 (*+*)val "[\"\n(vs, [c, c_2, c_3, c_4])\"]"

 "y x =\nIntegral c_3 +\n         1 / (- 1 * EI) *\n         (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3) D x";

   = return_discern_type_subst_4 |> Subst.to_string @{context}

 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =

 "y x =\nc_4 + c_3 * x +\n1 / (- 1 * EI) *\n(c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)";

 (*-------------------- contine discern_feedback_subst ----------------------------------------*)

 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =

 val return_discern_feedback_subst_4 = return_discern_type_subst_4

    "y x =\nc_4 + c_3 * x +\n1 / (- 1 * EI) *\n(c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)";

 (*-------------------- contine mk_env_subst_DEL ----------------------------------------------*)

 val (p,_,f,nxt,_,pt) = me nxt p c pt; 

 val return_mk_env_subst_DEL_4 = return_discern_feedback_subst_4  

 if f2str f =

 (*+*)val "[\"\n(vs, [c, c_2, c_3, c_4])\"]"

    "[Q x = c + - 1 * q_0 * x, M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n dy x =\n c_3 + 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n y x =\n c_4 + c_3 * x +\n 1 / (- 1 * EI) *\n (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]"

   = return_mk_env_subst_DEL_4 |> Subst.to_string @{context}

 then case nxt of ("End_Proof'", End_Proof') => ()

 (*\\\################# nth 4 equal_descr_pairs ############################################=//*)

   | _ => error "biegelinie.sml met2 e 1"

 else error "biegelinie.sml met2 e 2";

 (*///################# nth 7 equal_descr_pairs ############################################=\\*)

 =============================================================================================//*)

        val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))

         => (discern_feedback_subst id feedb) (*|> map fst (*rhs dropped*)|> map (pair id)*) ) (nth 7 equal_descr_pairs);

 "~~~~~ fun xxx , args:"; val ((_, (_, id)), (_, _, _, _, (feedb, _))) = (nth 7 equal_descr_pairs);

 (*--------------------------------------------------------------------------^^^----------------*)

  Pre_Conds.discern_feedback_subst id feedb;

 "~~~~~ fun discern_feedback_subst , args:"; val (id, Cor_TEST ((descr, (*[*)ts(*]*)), _)) = (id, feedb);

 (*+*)val (Free ("r_b", _), "[[y 0 = 0], [y L = 0], [M_b 0 = 0], [M_b L = 0]]")

   = (id, ts |> UnparseC.terms @{context});

     (*if*) fold (curry and_) (map TermC.is_list ts) true (*then*);

       val ts = ts;

            discern_type_subst (descr, id) ts;

 "~~~~~ fun discern_type_subst , args:"; val ((descr, id), ts) = ((descr, id), ts);

 val (Type ("fun", [Type ("List.list", [Type ("HOL.bool", [])]), _])) =

   (*case*) type_of descr (*of*);

          (*if*) TermC.is_list (hd ts) (*then*);

 val return_discern_type_subst_7 =

 (*       if TermC.is_list (hd ts)

          then*) [(id, ts |> map TermC.the_single |> TermC.list2isalist HOLogic.boolT)]

 (*       else []*)

 (*+*)val "[\"\n(r_b, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0])\"]"

   = return_discern_type_subst_7 |> Subst.to_string @{context}

 (*-------------------- contine discern_feedback_subst ----------------------------------------*)

 val return_discern_feedback_subst_7 = return_discern_type_subst_7

 (*-------------------- contine mk_env_subst_DEL ----------------------------------------------*)

 val return_mk_env_subst_DEL_7 = return_discern_type_subst_7

 (*+*)val "[\"\n(r_b, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0])\"]"

   = return_mk_env_subst_DEL_7 |> Subst.to_string @{context};

 (*\\\################# nth 7 equal_descr_pairs ############################################=//*)

 (*BEFORE correct (vs, [c, c_2, c_3, c_4])* )

 (*+*)val "[\"\n(l_l, L)\", \"\n(q_q, q_0)\", \"\n(fun_var, x)\", \"\n(vs, vs)\", \"\n(id_der, dy)\", \"\n(b_b, y)\"]"

 (*ERRORs still -----------------------------------------------------------^^^-------------------------------------, r_b*)

   = (env_subst |> Subst.to_string @{context})

 *)

 (*NOW only nth 7 is missing.. (but mk_env_eval_DEL completely broken)* )

 (*+*)val "[\"\n(l_l, L)\", \"\n(q_q, q_0)\", \"\n(fun_var, x)\", \"\n(vs, [c, c_2, c_3, c_4])\", \"\n(id_der, dy)\", \"\n(b_b, y)\"]"

 (*ERRORs still ---------------------------------------------------------------------------------------------------------------------, r_b*)

   = (env_subst |> Subst.to_string @ {context})

 *)                            

 (*+*)if (env_subst |> Subst.to_string @{context}) = "[\"\n" ^

 (*1*)"(l_l, L)\", \"\n" ^

 (*2*)"(q_q, q_0)\", \"\n" ^

 (*3*)"(fun_var, x)\", \"\n" ^

 (*4*)"(vs, [c, c_2, c_3, c_4])\", \"\n" ^

 (*5*)"(id_der, dy)\", \"\n" ^

 (*6*)"(b_b, y)\", \"\n" ^

 (*7*)"(r_b, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0])\"]"

 (*+*)then () else error "env_subst CHANGED";

 (*+*)if (i_model_max |> I_Model.to_string_TEST @{context}) = "[\n" ^

   "(1, [1], true ,#Given, (Cor_TEST Traegerlaenge L ,(l_l, [L]), Position.T)), \n" ^

   "(2, [1], true ,#Given, (Cor_TEST Streckenlast q_0 ,(q_q, [q_0]), Position.T)), \n" ^

   "(3, [1], true ,#Find, (Cor_TEST Biegelinie y ,(b_b, [y]), Position.T)), \n" ^

   "(4, [1], true ,#Relate, (Cor_TEST Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] ,(r_b, [[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]]), Position.T)), \n" ^

   "(5, [1], true ,#Given, (Cor_TEST FunktionsVariable x ,(fun_var, [x]), Position.T)), \n" ^

   "(6, [1], true ,#Given, (Cor_TEST GleichungsVariablen [c, c_2, c_3, c_4] ,(vs, [[c, c_2, c_3, c_4]]), Position.T)), \n" ^

   "(7, [1], true ,#Given, (Cor_TEST AbleitungBiegelinie dy ,(id_der, [dy]), Position.T))]"

 (*+*)then () else error "i_model_max CHANGED";

 (*||------------------ continue of_max_variant ---------------------------------------------\\*)

            mk_env_eval_DEL i_model_max;

 (*///----------------- step into mk_env_eval_DEL -------------------------------------------\\*)

 "~~~~~ fun mk_env_eval_DEL , args:"; val (i_singles) = (i_model_max);

        val xxx = (fn (_, _, _, _, (feedb, _)) => discern_feedback_subst id feedb);

 (*///################# nth 1 i_model_max \<longrightarrow>[], <>[] only in maximum-example ##############=\\*)

 "~~~~~ fun xxx , args:"; val (_, _, _, _, (feedb, _)) = nth 1 i_model_max;

 (*---------------------------------------------------------^^^------------*)

 (*+*)val "Cor_TEST Traegerlaenge L ,(l_l, [L])"

   = feedb |> I_Model.feedback_to_string'_TEST @{context};

            discern_feedback_subst id feedb;

 "~~~~~ fun discern_feedback_subst , args:"; val (Model_Def.Cor_TEST ((descr, [ts]), _)) = (feedb);

       (*if*) TermC.is_list ts (*else*);

       val ts = (*if TermC.is_list ts then TermC.isalist2list ts else*) [ts];

  Pre_Conds.discern_type_eval descr ts;

 "~~~~~ fun discern_type_eval , args:"; val (descr, ts) = (descr, ts);

 val _(*"real \<Rightarrow> una"*) =

   (*case*) type_of descr (*of*) 

 ;

  Pre_Conds.discern_atoms ts;

 "~~~~~ fun discern_atoms , args:"; val (ts) = (ts);

   (*if*) all_atoms ts (*then*);

 val return_distinguish_ts_eval_1 =

     map (rpair TermC.empty (*dummy rhs*)) ts

 (*-------------------- contine discern_type_subst --------------------------------------------*)

 (*-------------------- contine discern_feedback_subst ----------------------------------------*)

 (*-------------------- contine mk_env_eval_DEL -----------------------------------------------*)

 val return_mk_env_subst_DEL_1

   = filter_out (fn (_, b) => b = TermC.empty) return_distinguish_ts_eval_1

 (*+*)val [] = return_mk_env_subst_DEL_1

 (*\\\################# nth 1 i_model_max \<longrightarrow>[], <>[] only in maximum-example ##############=//*)

 (*\\\----------------- step into mk_env_eval_DEL -------------------------------------------//*)

 (*|||----------------- contine of_max_variant ------------------------------------------------*)

 (*  val env_eval = mk_env_eval_DEL  i_model_max*)

     val env_eval = mk_env_eval_DEL  i_model_max

 (*+*)val [] = env_eval

 val return_of_max_variant_step = (i_model_max, env_model, (env_subst, env_eval))

 ;

 return_of_max_variant_step = return_of_max_variant

 ( *\\\\\############### old test code ##################################################//////*)

 \<close> ML \<open>

 (*\\\----------------- step into of_max_variant --------------------------------------------//*)

     val (_, env_model, (env_subst, env_eval)) = return_of_max_variant

 (*|------------------- contine init_pstate ---------------------------------------------------*)

     val actuals = map snd env_model

 (*+* )val "[L, q_0, x, [c, c_2, c_3, c_4], dy, y, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]]"

   = actuals |> UnparseC.terms @{context}(**)

 (*+*)val 7 = length actuals( **)

 (*WRONG ----------------v-v--v---v--v---v--v---v-----------v-------v--v-------v--v---------v--v---------v*)

 (*+*) val "[L, q_0, x, [[c], [c_2], [c_3], [c_4]], dy, y, [[y 0 = 0], [y L = 0], [M_b 0 = 0], [M_b L = 0]]]"

   = actuals |> UnparseC.terms @{context}

 \<close> ML \<open>

     val formals = Program.formal_args prog

 (*+*)val "[l_l, q_q, fun_var, b_b, r_b, vs, id_der]"

   = formals |> UnparseC.terms @{context}

 (*+*)val 7 = length formals

 \<close> ML \<open>

     val preconds = Pre_Conds.check_from_store ctxt where_rls where_ env_subst env_eval

 \<close> text \<open> (*ERROR type_of: real/real list/(#) [c_4]*)

     val ctxt = ctxt |> ContextC.insert_assumptions (map snd (snd preconds));

     val ist = Istate.e_pstate

       |> Istate.set_eval prog_rls

       |> Istate.set_env_true (relate_args [] formals actuals ctxt prog met_id formals actuals)

 \<close> text \<open> (*ERROR type_of: real/real list/(#) [c_4]*)

 (*+*)(relate_args [] formals actuals ctxt prog met_id formals actuals)

 \<close> text \<open>

 val return_init_pstate = (Istate.Pstate ist, ctxt, program)

 \<close> ML \<open>(*\\------------ step into init_pstate -----------------------------------------------//*)

 (*\\------------------ step into init_pstate -----------------------------------------------//*)

 \<close> ML \<open>(*\------------- step into me_Add_Given_AbleitungBieg --------------------------------//*)

 (*\------------------- step into me_Add_Given_AbleitungBieg --------------------------------//*)

 \<close> text \<open> (*\------------ step into me_Add_Given_AbleitungBieg --------------------------------//*)

 val (p,_,f,nxt,_,pt) = return_Add_Given_AbleitungBieg;

                                                  val Apply_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt

 \<close> text \<open>

 (* final test ... ----------------------------------------------------------------------------*)

 (*+*)val ([], Met) = p

 (*+*)val Apply_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt

 \<close> ML \<open>