1.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Fri Sep 03 17:19:20 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Mon Sep 06 14:48:38 2010 +0200
     1.3 @@ -3436,12 +3436,13 @@
     1.4  (*-------------------18.3.03 --> struct <-----------vvv--*)
     1.5  val add_fractions_p = common_nominator_p; (*FIXXXME:eilig f"ur norm_Rational*)
     1.6  
     1.7 -(*.discard binary minus, shift unary minus into -1*; 
     1.8 +(*WN100906 removed in favour of discard_minus = discard_minus_ formerly 
     1.9 +   discard binary minus, shift unary minus into -1*; 
    1.10     unary minus before numerals are put into the numeral by parsing;
    1.11 -   contains absolute minimum of thms for context in norm_Rational .*)
    1.12 +   contains absolute minimum of thms for context in norm_Rational
    1.13  val discard_minus = prep_rls(
    1.14    Rls {id = "discard_minus", preconds = [], rew_ord = ("dummy_ord",dummy_ord), 
    1.15 -      erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)
    1.16 +      erls = e_rls, srls = Erls, calc = [],
    1.17        rules = [Thm ("real_diff_minus", num_str @{thm real_diff_minus}),
    1.18  	       (*"a - b = a + -1 * b"*)
    1.19  	       Thm ("sym_real_mult_minus1",
    1.20 @@ -3450,6 +3451,8 @@
    1.21  	       ],
    1.22        scr = EmptyScr
    1.23        }):rls;
    1.24 + *)
    1.25 +
    1.26  (*erls for calculate_Rational; make local with FIXX@ME result:term *term list*)
    1.27  val powers_erls = prep_rls(
    1.28    Rls {id = "powers_erls", preconds = [], rew_ord = ("dummy_ord",dummy_ord), 
    1.29 @@ -3729,7 +3732,7 @@
    1.30     Seq {id = "norm_Rational"(*_mg*), preconds = [], 
    1.31         rew_ord = ("dummy_ord",dummy_ord), 
    1.32         erls = norm_rat_erls, srls = Erls, calc = [],
    1.33 -       rules = [Rls_ discard_minus1,
    1.34 +       rules = [Rls_ discard_minus,
    1.35  		Rls_ rat_mult_poly,(* removes double fractions like a/b/c    *)
    1.36  		Rls_ make_rat_poly_with_parentheses, (*WN0510 also in(#)below*)
    1.37  		Rls_ cancel_p_rls, (*FIXME.MG:cancel_p does NOT order sometim*)
    1.38 @@ -3801,7 +3804,7 @@
    1.39  				       eval_is_ratpolyexp "")],
    1.40  		crls = e_rls, nrls = norm_Rational_rls},
    1.41  "Script SimplifyScript (t_t::real) =                             " ^
    1.42 -"  ((Try (Rewrite_Set discard_minus1 False) @@                   " ^
    1.43 +"  ((Try (Rewrite_Set discard_minus False) @@                   " ^
    1.44  "    Try (Rewrite_Set rat_mult_poly False) @@                    " ^
    1.45  "    Try (Rewrite_Set make_rat_poly_with_parentheses False) @@   " ^
    1.46  "    Try (Rewrite_Set cancel_p_rls False) @@                     " ^