src/Tools/isac/calcelems.sml
changeset 59257 a1daf71787b1
parent 59255 383722bfcff5
child 59263 0fde9446eda2
     1.1 --- a/src/Tools/isac/calcelems.sml	Thu Oct 27 10:48:24 2016 +0200
     1.2 +++ b/src/Tools/isac/calcelems.sml	Sat Nov 12 17:21:43 2016 +0100
     1.3 @@ -135,7 +135,8 @@
     1.4  | Rls_ of rls          (*.ie. rule sets may be nested.*)
     1.5  and scr =
     1.6      EmptyScr
     1.7 -  | Prog of term (* for met *)
     1.8 +  | Prog of term (* a leaf is either a tactic or an 'exp' in 'let v = expr' 
     1.9 +                    where 'exp' does not contain a tactic. *)
    1.10    | Rfuns of     (* for Rrls, usage see rational.sml ----- reverse rewrite -----      *)
    1.11      {init_state : (* initialise for reverse rewriting by the Interpreter              *)
    1.12        term ->         (* for this the rrlsstate is initialised:                       *)