1.1 --- a/src/Tools/isac/ProgLang/rewrite.sml	Sat Aug 17 15:45:36 2013 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml	Fri Aug 23 09:32:05 2013 +0200
     1.3 @@ -9,10 +9,41 @@
     1.4  exception NO_REWRITE;
     1.5  exception STOP_REW_SUB; (*WN050820 quick and dirty*)
     1.6  
     1.7 -(*17.6.00: rewrite by going down the term with rew_sub*)
     1.8 -(* val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
     1.9 -       (thy, 1, []:(Term.term * Term.term) list, rew_ord, erls, bool,thm,term);
    1.10 -   *)
    1.11 +(* 
    1.12 +Synopsis rewriting (prep for reference manual):
    1.13 +----------------------------------------------
    1.14 +Rewriting uses theorems for transforming terms. However, not all kinds
    1.15 +of such transformations can be done by rewriting. Examples are
    1.16 +calculation with numerals or cancellation of fractions. 
    1.17 +
    1.18 +Isac tries to present transformations like calculations or cancellation 
    1.19 +as simple rewrite steps for the naive user. However, some of such
    1.20 +transformations should be transparent to the user by single-stepping.
    1.21 +For instance, cancellation involves interesting CA algorithms like 
    1.22 +GCD of multivariate polynomials.
    1.23 +
    1.24 +Thus Isac has two mechanisms for including SML code, "thm Calc" and "Rrls",
    1.25 +the former for steps which are not meant to be inspected by single-stepping
    1.26 +the latter meant for single-stepping and providing respective mechanisms.
    1.27 +
    1.28 +(1) Inclusion by "thm Calc" for 1-step execution
    1.29 +TODO
    1.30 +
    1.31 +(2) Inclusion by "Rrls" for multi-step execution
    1.32 +TODO
    1.33 +In multi-step execution "reverse rewriting" worked only as passive presentation
    1.34 +without any interaction. So the functions init_state, locate_rule etc are just dummies.
    1.35 +TODO
    1.36 +? multi-step execution did never work.
    1.37 +what worked is "reverse rewriting", 
    1.38 +i.e. presentation of intermediate steps *without* interaction
    1.39 +TODO
    1.40 +# type rule and scr | Rfuns
    1.41 +# type rrlsstate = (*state for reverse rewriting*) 
    1.42 +# type and rls | Rrls
    1.43 +all in calcelems.sml
    1.44 +TODO
    1.45 +*)
    1.46  fun rewrite__ thy i bdv tless rls put_asm thm ct =
    1.47    (let
    1.48      val (t',asms,lrd,rew) =