1.1 --- a/src/sml/IsacKnowledge/Biegelinie.ML	Sat Sep 16 23:07:37 2006 +0200
     1.2 +++ b/src/sml/IsacKnowledge/Biegelinie.ML	Sun Sep 17 00:06:07 2006 +0200
     1.3 @@ -261,7 +261,11 @@
     1.4  				   Thm ("not_false",num_str not_false)], 
     1.5  		calc = [], 
     1.6  		srls = append_rls "erls_IntegrierenUndK.." e_rls 
     1.7 -				  [Calc("Tools.rhs", eval_rhs"eval_rhs_")],
     1.8 +				  [Calc("Tools.rhs", eval_rhs"eval_rhs_"),
     1.9 +				   Thm ("last_thm",num_str last_thm),
    1.10 +				   Thm ("if_True",num_str if_True),
    1.11 +				   Thm ("if_False",num_str if_False)
    1.12 +				   ],
    1.13  		prls = Erls, crls = Atools_erls, nrls = Erls},
    1.14  "Script Biegelinie2Script                                                 \
    1.15  \(l_::real) (q_::real) (v_::real) (b_::real=>real) (rb_::bool list) =     \
    1.16 @@ -273,13 +277,13 @@
    1.17  \      (equs_::bool list) =                                               \
    1.18  \             (SubProblem (Biegelinie_,[setzeRandbedingungen,Biegelinien],\
    1.19  \                          [Biegelinien,setzeRandbedingungenEin])         \
    1.20 -\                          [booll_ funs_, booll_ rb_]);                     \
    1.21 +\                          [booll_ funs_, booll_ rb_]);                   \
    1.22  \      (cons_::bool list) =                                               \
    1.23  \             (SubProblem (Biegelinie_,[linear,system],[no_met])          \
    1.24  \                          [booll_ equs_, reall [c,c_2,c_3,c_4]]);        \
    1.25 -\       B_ = Take (last_elem funs_);                                      \
    1.26 +\       B_ = Take (last funs_);                                           \
    1.27  \       B_ = ((Substitute cons_) @@                                       \
    1.28 -\              (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B_    \
    1.29 +\              (Rewrite_Set_Inst [(bdv, v_)] make_ratpoly_in False)) B_   \
    1.30  \ in B_)"
    1.31  ));
    1.32  
    1.33 @@ -437,7 +441,6 @@
    1.34  \      equ_ = (Substitute [bdv_ = val_]) fun_;       \
    1.35  \      equ_ = (Substitute [sub_]) fun_               \
    1.36  \ in (Rewrite_Set norm_Rational False) equ_)             "
    1.37 -(*FIXME.WN060901. scr-interpreter ERROR in nxt_tac without Take above !*)
    1.38  ));
    1.39  
    1.40  

     2.1 --- a/src/smltest/IsacKnowledge/biegelinie.sml	Sat Sep 16 23:07:37 2006 +0200
     2.2 +++ b/src/smltest/IsacKnowledge/biegelinie.sml	Sun Sep 17 00:06:07 2006 +0200
     2.3 @@ -877,7 +877,7 @@
     2.4  (*---vvv-NOTok--------------------------------------------------------------*)
     2.5  
     2.6  
     2.7 -"----- Bsp 7.27 with me";
     2.8 +"----- Bsp 7.70 with me";
     2.9  val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
    2.10  	     "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",
    2.11  	     "FunktionsVariable x"];
    2.12 @@ -911,19 +911,44 @@
    2.13  "further 'me' see ----- SubProblem (_,[vonBelastungZu,Biegelinien] -------\
    2.14  \                 ----- SubProblem (_,[setzeRandbedingungen,Biegelinien] -";
    2.15  
    2.16 -"----- Bsp 7.27 with autoCalculate";
    2.17 +"----- Bsp 7.70 with autoCalculate";
    2.18  states:=[];
    2.19  CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
    2.20 -	     "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",
    2.21 +	     "Randbedingungen [Q 0 = q_0 * L, M_b L = 0, y 0 = 0, y' 0 = 0]",
    2.22  	     "FunktionsVariable x"],
    2.23  	    ("Biegelinie.thy", ["Biegelinien"],
    2.24  		     ["IntegrierenUndKonstanteBestimmen2"]))];
    2.25  moveActiveRoot 1;
    2.26 +autoCalculate 1 CompleteCalc;
    2.27 +val ((pt,_),_) = get_calc 1;show_pt pt;
    2.28 +val is = get_istate pt ([],Res); writeln (istate2str is);
    2.29 +
    2.30 +val t = str2term " last                                                     \
    2.31 +\[Q x = L * q_0 + -1 * q_0 * x,                                              \
    2.32 +\ M_b x = -1 * q_0 * L ^^^ 2 / 2 + q_0 * L / 1 * x + -1 * q_0 / 2 * x ^^^ 2,\
    2.33 +\ y' x =                                                                    \
    2.34 +\  -3 * q_0 * L ^^^ 2 / (-6 * EI) * x + 3 * L * q_0 / (-6 * EI) * x ^^^ 2 +\
    2.35 +\  -1 * q_0 / (-6 * EI) * x ^^^ 3,                                         \
    2.36 +\ y x =                                                                    \
    2.37 +\  -6 * q_0 * L ^^^ 2 / (-24 * EI) * x ^^^ 2 +                              \
    2.38 +\  4 * L * q_0 / (-24 * EI) * x ^^^ 3 +                                     \
    2.39 +\  -1 * q_0 / (-24 * EI) * x ^^^ 4]";
    2.40 +val srls = append_rls "erls_IntegrierenUndK.." e_rls 
    2.41 +		      [Calc("Tools.rhs", eval_rhs"eval_rhs_"),
    2.42 +		       Calc ("op =",eval_equal "#equal_"),
    2.43 +		       Thm ("refl",num_str refl),
    2.44 +		       Thm ("last_thm",num_str last_thm),
    2.45 +		       Thm ("if_True",num_str if_True),
    2.46 +		       Thm ("if_False",num_str if_False)
    2.47 +		       ]
    2.48 +		      ;
    2.49 +val t = str2term "last [1,2,3,4]";
    2.50 +trace_rewrite := true;
    2.51 +val Some (e1__,_) = rewrite_set_ thy false srls t;
    2.52 +trace_rewrite := false;
    2.53 +term2str e1__;
    2.54 +
    2.55  trace_script := true;
    2.56 -autoCalculate 1 CompleteCalcHead;val ((pt,_),_) = get_calc 1;show_pt pt;
    2.57 -(*
    2.58 -autoCalculate 1 CompleteCalc; 
    2.59 -*)
    2.60  trace_script := false;
    2.61  
    2.62