1.1 --- a/src/sml/IsacKnowledge/AlgEin.ML	Tue Apr 10 23:45:07 2007 +0200
     1.2 +++ b/src/sml/IsacKnowledge/AlgEin.ML	Thu Apr 12 16:11:11 2007 +0200
     1.3 @@ -88,26 +88,26 @@
     1.4  \      t_ = Substitute [oben = sum_] t_;\
     1.5  \      t_ = Substitute o_ t_;\
     1.6  \      t_ = Substitute [k_, q__] t_;\
     1.7 -\      t_ = (Repeat (Try (Rewrite_Set norm_Rational False))) t_;\
     1.8 +\      t_ = (Repeat (Try (Rewrite_Set norm_Poly False))) t_;\
     1.9  \      sum_ = boollist2sum s_;\
    1.10  \      t_ = Substitute [senkrecht = sum_] t_;\
    1.11  \      t_ = Substitute s_ t_;\
    1.12  \      t_ = Substitute [k_, q__] t_;\
    1.13 -\      t_ = (Repeat (Try (Rewrite_Set norm_Rational False))) t_;\
    1.14 +\      t_ = (Repeat (Try (Rewrite_Set norm_Poly False))) t_;\
    1.15  \      sum_ = boollist2sum u_;\
    1.16  \      t_ = Substitute [unten = sum_] t_;\
    1.17  \      t_ = Substitute u_ t_;\
    1.18  \      t_ = Substitute [k_, q__] t_;\
    1.19 -\      t_ = (Repeat (Try (Rewrite_Set norm_Rational False))) t_\
    1.20 -\ in (Try (Rewrite_Set norm_Rational False)) t_)"
    1.21 +\      t_ = (Repeat (Try (Rewrite_Set norm_Poly False))) t_\
    1.22 +\ in (Try (Rewrite_Set norm_Poly False)) t_)"
    1.23  ));
    1.24  
    1.25  store_met
    1.26      (prep_met AlgEin.thy "met_algein_symnum" [] e_metID
    1.27  	      (["Berechnung","erstSymbolisch"],
    1.28  	       [("#Given" ,["KantenLaenge k_","Querschnitt q__",
    1.29 -			    "Kantenunten u_", "Kantensenkrecht s_", 
    1.30 -			    "Kantenoben o_"]),
    1.31 +			    "KantenUnten u_", "KantenSenkrecht s_", 
    1.32 +			    "KantenOben o_"]),
    1.33  		("#Find"  ,["GesamtLaenge l_"])
    1.34  		],
    1.35  	       {rew_ord'="tless_true", rls'= e_rls, calc = [], 
    1.36 @@ -122,17 +122,17 @@
    1.37  \      sum_ = boollist2sum o_;\
    1.38  \      t_ = Substitute [oben = sum_] t_;\
    1.39  \      t_ = Substitute o_ t_;\
    1.40 -\      t_ = (Repeat (Try (Rewrite_Set norm_Rational False))) t_;\
    1.41 +\      t_ = (Repeat (Try (Rewrite_Set norm_Poly False))) t_;\
    1.42  \      sum_ = boollist2sum s_;\
    1.43  \      t_ = Substitute [senkrecht = sum_] t_;\
    1.44  \      t_ = Substitute s_ t_;\
    1.45 -\      t_ = (Repeat (Try (Rewrite_Set norm_Rational False))) t_;\
    1.46 +\      t_ = (Repeat (Try (Rewrite_Set norm_Poly False))) t_;\
    1.47  \      sum_ = boollist2sum u_;\
    1.48  \      t_ = Substitute [unten = sum_] t_;\
    1.49  \      t_ = Substitute u_ t_;\
    1.50 -\      t_ = (Repeat (Try (Rewrite_Set norm_Rational False))) t_;\
    1.51 +\      t_ = (Repeat (Try (Rewrite_Set norm_Poly False))) t_;\
    1.52  \      t_ = Substitute [k_, q__] t_\
    1.53 -\ in (Try (Rewrite_Set norm_Rational False)) t_)"
    1.54 +\ in (Try (Rewrite_Set norm_Poly False)) t_)"
    1.55  ));
    1.56  
    1.57  (* show_mets();

     2.1 --- a/src/smltest/IsacKnowledge/algein.sml	Tue Apr 10 23:45:07 2007 +0200
     2.2 +++ b/src/smltest/IsacKnowledge/algein.sml	Thu Apr 12 16:11:11 2007 +0200
     2.3 @@ -113,6 +113,8 @@
     2.4  moveActiveRoot 1;
     2.5  autoCalculate 1 CompleteCalc;
     2.6  val ((pt,p),_) = get_calc 1; show_pt pt;
     2.7 +if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "L = 104" then()
     2.8 +else raise error "algein.sml: 'Berechnung' 'erstSymbolisch' changed";
     2.9  
    2.10  (*
    2.11  show_pt pt;