1.1 --- a/src/sml/IsacKnowledge/Atools.thy	Sun Sep 17 00:06:07 2006 +0200
     1.2 +++ b/src/sml/IsacKnowledge/Atools.thy	Sun Sep 17 00:32:14 2006 +0200
     1.3 @@ -46,6 +46,7 @@
     1.4  (*-------------------- rules -------------------------------------*)
     1.5  rules (*for evaluating the assumptions of conditional rules*)
     1.6  
     1.7 +  last_thmI	"lastI (x#xs) = (if xs =!= [] then x else lastI xs)"
     1.8    real_unari_minus           "- a = (-1) * a"
     1.9  
    1.10    rle_refl                  "(n::real) <= n"

     2.1 --- a/src/sml/IsacKnowledge/Biegelinie.ML	Sun Sep 17 00:06:07 2006 +0200
     2.2 +++ b/src/sml/IsacKnowledge/Biegelinie.ML	Sun Sep 17 00:32:14 2006 +0200
     2.3 @@ -262,7 +262,8 @@
     2.4  		calc = [], 
     2.5  		srls = append_rls "erls_IntegrierenUndK.." e_rls 
     2.6  				  [Calc("Tools.rhs", eval_rhs"eval_rhs_"),
     2.7 -				   Thm ("last_thm",num_str last_thm),
     2.8 +				   Calc ("Atools.ident",eval_ident "#ident_"),
     2.9 +				   Thm ("last_thmI",num_str last_thmI),
    2.10  				   Thm ("if_True",num_str if_True),
    2.11  				   Thm ("if_False",num_str if_False)
    2.12  				   ],
    2.13 @@ -281,7 +282,7 @@
    2.14  \      (cons_::bool list) =                                               \
    2.15  \             (SubProblem (Biegelinie_,[linear,system],[no_met])          \
    2.16  \                          [booll_ equs_, reall [c,c_2,c_3,c_4]]);        \
    2.17 -\       B_ = Take (last funs_);                                           \
    2.18 +\       B_ = Take (lastI funs_);                                           \
    2.19  \       B_ = ((Substitute cons_) @@                                       \
    2.20  \              (Rewrite_Set_Inst [(bdv, v_)] make_ratpoly_in False)) B_   \
    2.21  \ in B_)"

     3.1 --- a/src/sml/IsacKnowledge/PolyEq.ML	Sun Sep 17 00:06:07 2006 +0200
     3.2 +++ b/src/sml/IsacKnowledge/PolyEq.ML	Sun Sep 17 00:32:14 2006 +0200
     3.3 @@ -1145,6 +1145,7 @@
     3.4  	       Rls_ order_add_mult_in,
     3.5  	       Rls_ discard_parentheses,
     3.6  	       Rls_ separate_bdvs,
     3.7 +	       (* Rls_ rearrange_assoc, WN060916 why does cancel_p not work?*)
     3.8  	       Rls_ cancel_p
     3.9  	       (*Calc ("HOL.divide"  ,eval_cancel "#divide_") too weak!*)
    3.10  	       ],

     4.1 --- a/src/smltest/IsacKnowledge/biegelinie.sml	Sun Sep 17 00:06:07 2006 +0200
     4.2 +++ b/src/smltest/IsacKnowledge/biegelinie.sml	Sun Sep 17 00:32:14 2006 +0200
     4.3 @@ -935,9 +935,8 @@
     4.4  \  -1 * q_0 / (-24 * EI) * x ^^^ 4]";
     4.5  val srls = append_rls "erls_IntegrierenUndK.." e_rls 
     4.6  		      [Calc("Tools.rhs", eval_rhs"eval_rhs_"),
     4.7 -		       Calc ("op =",eval_equal "#equal_"),
     4.8 -		       Thm ("refl",num_str refl),
     4.9 -		       Thm ("last_thm",num_str last_thm),
    4.10 +		       Calc ("Atools.ident",eval_ident "#ident_"),
    4.11 +		       Thm ("last_thmI",num_str last_thmI),
    4.12  		       Thm ("if_True",num_str if_True),
    4.13  		       Thm ("if_False",num_str if_False)
    4.14  		       ]