62 |
62 |
63 ML> ... |
63 ML> ... |
64 ML> val c = (the o (parse thy)) s; |
64 ML> val c = (the o (parse thy)) s; |
65 val c = |
65 val c = |
66 "Script make_fun_by_new_variable = |
66 "Script make_fun_by_new_variable = |
67 Input [Real f_, Real v_v, BoolList eqs_] |
67 Input [Real f_f, Real v_v, BoolList eqs] |
68 Local [Bool h_, BoolList es_, RealList vs_, Real v1_, Real v2_, Bool e1, |
68 Local [Bool h_, BoolList es_, RealList vs_, Real v1_, Real v2_, Bool e1, |
69 Bool e2_, BoolList s_1, BoolList s_2] |
69 Bool e2_, BoolList s_1, BoolList s_2] |
70 Tacs [SEQU |
70 Tacs [SEQU |
71 [let h_ = (hd o filter (Testvar m_)) eqs_; es_ = eqs_ -- [h_]; |
71 [let h_ = (hd o filter (Testvar m_)) eqs; es_ = eqs -- [h_]; |
72 vs_ = Var h_ -- [f_]; v1_ = Nth #1 vs_; v2_ = Nth #2 vs_; |
72 vs_ = Var h_ -- [f_]; v1_ = Nth #1 vs_; v2_ = Nth #2 vs_; |
73 e1_ = (hd o filter (Testvar v1_)) es_; |
73 e1_ = (hd o filter (Testvar v1_)) es_; |
74 e2_ = (hd o filter (Testvar v2_)) es_ |
74 e2_ = (hd o filter (Testvar v2_)) es_ |
75 in Subproblem Spec (R, [univar, equation], no_met) |
75 in Subproblem Spec (R, [univar, equation], no_met) |
76 InOut [In e1_, In v1_, Out s_1] ; |
76 InOut [In e1_, In v1_, Out s_1] ; |
82 |
82 |
83 ML> ... |
83 ML> ... |
84 ML> val c = (the o (parse thy)) s; |
84 ML> val c = (the o (parse thy)) s; |
85 val c = |
85 val c = |
86 "Script make_fun_explicit = |
86 "Script make_fun_explicit = |
87 Input [Real f_, Real v_v, BoolList eqs_] |
87 Input [Real f_f, Real v_v, BoolList eqs] |
88 Local [Bool h_, Bool eq_, RealList vs_, Real v1_, BoolList ss_] |
88 Local [Bool h_, Bool eq_, RealList vs_, Real v1_, BoolList ss_] |
89 Tacs [SEQU |
89 Tacs [SEQU |
90 [let h_ = (hd o filter (Testvar m_)) eqs_; eq_ = hd (eqs_ -- [h_]); |
90 [let h_ = (hd o filter (Testvar m_)) eqs; eq_ = hd (eqs -- [h_]); |
91 vs_ = Var h_ -- [f_]; v1_ = hd (vs_ -- [v_]) |
91 vs_ = Var h_ -- [f_]; v1_ = hd (vs_ -- [v_]) |
92 in Subproblem Spec (R, [univar, equation], no_met) |
92 in Subproblem Spec (R, [univar, equation], no_met) |
93 InOut [In eq_, In v1_, Out ss_]], |
93 InOut [In eq_, In v1_, Out ss_]], |
94 Take (Bool h_) ; Substitute [(v1_, (Rhs o hd) ss_)]] |
94 Take (Bool h_) ; Substitute [(v1_, (Rhs o hd) ss_)]] |
95 Return [Currform]" : cterm |
95 Return [Currform]" : cterm |