4 (c) due to copyright terms |
4 (c) due to copyright terms |
5 |
5 |
6 use"IsacKnowledge/Biegelinie.ML"; |
6 use"IsacKnowledge/Biegelinie.ML"; |
7 use"Biegelinie.ML"; |
7 use"Biegelinie.ML"; |
8 |
8 |
|
9 remove_thy"Typefix"; |
9 remove_thy"Biegelinie"; |
10 remove_thy"Biegelinie"; |
10 use_thy"IsacKnowledge/Isac"; |
11 use_thy"IsacKnowledge/Isac"; |
11 *) |
12 *) |
12 |
13 |
13 (** interface isabelle -- isac **) |
14 (** interface isabelle -- isac **) |
106 [["Biegelinien","setzeRandbedingungenEin"]])); |
107 [["Biegelinien","setzeRandbedingungenEin"]])); |
107 |
108 |
108 store_pbt |
109 store_pbt |
109 (prep_pbt Biegelinie.thy "pbl_equ_fromfun" [] e_pblID |
110 (prep_pbt Biegelinie.thy "pbl_equ_fromfun" [] e_pblID |
110 (["makeFunctionTo","equation"], |
111 (["makeFunctionTo","equation"], |
111 [("#Given" ,["functionEq funs_","substitution subs_"]), |
112 [("#Given" ,["functionEq fun_","substitution sub_"]), |
112 ("#Find" ,["equality equ___"])], |
113 ("#Find" ,["equality equ___"])], |
113 append_rls "e_rls" e_rls [], |
114 append_rls "e_rls" e_rls [], |
114 None, |
115 None, |
115 [(*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)["",""]])); |
116 [["Equation","fromFunction"]])); |
116 |
117 |
117 |
118 |
118 |
119 |
119 (** methods **) |
120 (** methods **) |
120 |
121 |
348 prls=e_rls, |
349 prls=e_rls, |
349 crls = Atools_erls, nrls = e_rls}, |
350 crls = Atools_erls, nrls = e_rls}, |
350 "empty_script" |
351 "empty_script" |
351 )); |
352 )); |
352 |
353 |
|
354 store_met |
|
355 (prep_met Biegelinie.thy "met_equ" [] e_metID |
|
356 (["Equation"], |
|
357 [], |
|
358 {rew_ord'="tless_true", rls'=Erls, calc = [], |
|
359 srls = e_rls, |
|
360 prls=e_rls, |
|
361 crls = Atools_erls, nrls = e_rls}, |
|
362 "empty_script" |
|
363 )); |
|
364 |
|
365 store_met |
|
366 (prep_met Biegelinie.thy "met_equ_fromfun" [] e_metID |
|
367 (["Equation","fromFunction"], |
|
368 [("#Given" ,["functionEq fun_","substitution sub_"]), |
|
369 ("#Find" ,["equality equ___"])], |
|
370 {rew_ord'="tless_true", rls'=Erls, calc = [], |
|
371 srls = append_rls "srls_in_EquationfromFunc" e_rls |
|
372 [Calc("Tools.lhs", eval_lhs"eval_lhs_"), |
|
373 Calc("Atools.argument'_in", |
|
374 eval_argument_in |
|
375 "Atools.argument'_in")], |
|
376 prls=e_rls, |
|
377 crls = Atools_erls, nrls = e_rls}, |
|
378 (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) --> |
|
379 0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*) |
|
380 "Script Function2Equality (fun_::bool) (sub_::bool) =\ |
|
381 \ (let fun_ = Take fun_; \ |
|
382 \ bdv_ = argument_in (lhs fun_); \ |
|
383 \ val_ = argument_in (lhs sub_); \ |
|
384 \ equ_ = (Substitute [bdv_ = val_]) fun_; \ |
|
385 \ equ_ = (Substitute [sub_]) fun_ \ |
|
386 \ in (Rewrite_Set norm_Poly False) equ_) " |
|
387 (*FIXME.WN060901.ERROR in nxt_tac without Take above !?!*) |
|
388 )); |
|
389 |
|
390 |
|
391 |
353 (* use"Biegelinie.ML"; |
392 (* use"Biegelinie.ML"; |
354 *) |
393 *) |