1.1 --- a/doc/matauthor.txt	Tue Apr 10 13:54:39 2007 +0200
     1.2 +++ b/doc/matauthor.txt	Tue Apr 10 16:46:45 2007 +0200
     1.3 @@ -41,4 +41,42 @@
     1.4       bool_ (y L = 0)]
     1.5      b3_ =
     1.6     (M_b 0 = 0)'
     1.7 -without type errors at 3rd "@@@ next   leaf 'SubProblem...b3_ = ..." !!!
     1.8 \ No newline at end of file
     1.9 +without type errors at 3rd "@@@ next   leaf 'SubProblem...b3_ = ..." !!!
    1.10 +=============================================================================
    1.11 +WN070406 while 'programming' Rechnen
    1.12 +-----------------------------------------------------------------------------
    1.13 +the specification of an example should use Isac.thy !!!
    1.14 +here we had dI'=AlgEin.thy, and norm_Rational stopped, causing nxt = Empty_Tac:
    1.15 +#  rls: norm_Rational on: L = 1 + 2 + 3
    1.16 +##  rls: discard_minus_ on: L = 1 + 2 + 3
    1.17 +###  try thm: real_diff_minus
    1.18 +###  try thm: sym_real_mult_minus1
    1.19 +##  rls: rat_mult_poly on: L = 1 + 2 + 3
    1.20 +###  try thm: rat_mult_poly_l
    1.21 +###  try thm: rat_mult_poly_r
    1.22 +##  rls: make_rat_poly_with_parentheses on: L = 1 + 2 + 3
    1.23 +###  rls: discard_minus_ on: L = 1 + 2 + 3
    1.24 +####  try thm: real_diff_minus
    1.25 +####  try thm: sym_real_mult_minus1
    1.26 +###  rls: expand_poly_rat_ on: L = 1 + 2 + 3
    1.27 +####  try thm: real_plus_binom_pow4_poly
    1.28 +####  try thm: real_plus_binom_pow5_poly
    1.29 +####  try thm: real_plus_binom_pow2_poly
    1.30 +####  try thm: real_plus_binom_pow3_poly
    1.31 +####  try thm: real_plus_minus_binom1_p_p
    1.32 +####  try thm: real_plus_minus_binom2_p_p
    1.33 +####  try thm: real_add_mult_distrib_poly
    1.34 +####  try thm: real_add_mult_distrib2_poly
    1.35 +####  try thm: realpow_multI_poly
    1.36 +####  try thm: realpow_pow
    1.37 +###  try calc: op *'
    1.38 +###  rls: order_mult_rls_ on: L = 1 + 2 + 3
    1.39 +####  rls: order_mult_ on: L = 1 + 2 + 3
    1.40 +#######  rls: e_rls-is_multUnordered on: 1 + 2 + 3 is_multUnordered
    1.41 +########  try calc: Poly.is'_multUnordered'
    1.42 +val f = Form' (FormKF (~1, EdUndef, ...)) : mout
    1.43 +val nxt = ("Empty_Tac", Empty_Tac) : tac'_
    1.44 +-----------------------------------------------------------------------------
    1.45 +the pattern for eval_xxx must include the function-constant of the predicate,
    1.46 +because this is required for rewriting by 'xxx _ = value'
    1.47 +-----------------------------------------------------------------------------