71 "(0 ,[] ,false ,#Find ,Inc Biegelinie ,(??.empty, [])), \n" ^ |
71 "(0 ,[] ,false ,#Find ,Inc Biegelinie ,(??.empty, [])), \n" ^ |
72 "(0 ,[] ,false ,#Relate ,Inc Randbedingungen [] ,(??.empty, [])), \n" ^ |
72 "(0 ,[] ,false ,#Relate ,Inc Randbedingungen [] ,(??.empty, [])), \n" ^ |
73 "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L ,(l_l, [L]))]" |
73 "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L ,(l_l, [L]))]" |
74 (*+*)then () else error "INITIAL I_Model CHANGED"; |
74 (*+*)then () else error "INITIAL I_Model CHANGED"; |
75 |
75 |
76 val Add (2, [1], true, "#Given", Cor ((Const ("Biegelinie.Streckenlast", _), [Free ("q_0", _)]), |
76 val Add (2, [1], true, "#Given", Cor ((Const (\<^const_name>\<open>Streckenlast\<close>, _), [Free ("q_0", _)]), |
77 (Free ("q_q", _), [Free ("q_0", _)]))) = (*case*) |
77 (Free ("q_q", _), [Free ("q_0", _)]))) = (*case*) |
78 I_Model.check_single ctxt sel oris pbl ppc ct (*of*); |
78 I_Model.check_single ctxt sel oris pbl ppc ct (*of*); |
79 "~~~~~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, str) = (ctxt, sel, oris, pbl, ppc, ct); |
79 "~~~~~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, str) = (ctxt, sel, oris, pbl, ppc, ct); |
80 val SOME t =(*case*) TermC.parseNEW ctxt str (*of*); |
80 val SOME t =(*case*) TermC.parseNEW ctxt str (*of*); |
81 (** )val ("", (2, [1], "#Given", Const ("Biegelinie.Streckenlast", _), [Free ("q_0", _)]), [Free ("q_0", _)]) =( **) |
81 (** )val ("", (2, [1], "#Given", Const (\<^const_name>\<open>Streckenlast\<close>, _), [Free ("q_0", _)]), [Free ("q_0", _)]) =( **) |
82 (**)val ("", ori', all) =(**) |
82 (**)val ("", ori', all) =(**) |
83 (*case*) O_Model.is_known ctxt m_field o_model t (*of*); |
83 (*case*) O_Model.is_known ctxt m_field o_model t (*of*); |
84 |
84 |
85 (*+*)O_Model.single_to_string ori'; |
85 (*+*)O_Model.single_to_string ori'; |
86 (*+*)val [Free ("q_0", _)] = all; |
86 (*+*)val [Free ("q_0", _)] = all; |
87 |
87 |
88 (** )val ("", (2, [1], true, "#Given", Cor ((Const ("Biegelinie.Streckenlast", _), [Free ("q_0", _)]), (Free ("q_q", _), [Free ("q_0", _)])))) =( **) |
88 (** )val ("", (2, [1], true, "#Given", Cor ((Const (\<^const_name>\<open>Streckenlast\<close>, _), [Free ("q_0", _)]), (Free ("q_q", _), [Free ("q_0", _)])))) =( **) |
89 (**)val ("", itm) =(**) |
89 (**)val ("", itm) =(**) |
90 (*case*) is_notyet_input ctxt i_model all ori' m_patt (*of*); |
90 (*case*) is_notyet_input ctxt i_model all ori' m_patt (*of*); |
91 |
91 |
92 Add itm (*return from add_single*); |
92 Add itm (*return from add_single*); |
93 "~~~~~ from fun check_single \<longrightarrow>fun by_Add_ , return:"; val (I_Model.Add itm) = (Add itm); |
93 "~~~~~ from fun check_single \<longrightarrow>fun by_Add_ , return:"; val (I_Model.Add itm) = (Add itm); |