1.1 --- a/doc-src/IsarRef/Thy/Generic.thy	Tue Jun 03 17:03:50 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Generic.thy	Tue Jun 03 23:46:53 2008 +0200
     1.3 @@ -212,8 +212,8 @@
     1.4    indicate the positions to substitute at.  Positions are ordered from
     1.5    the top of the term tree moving down from left to right. For
     1.6    example, in @{text "(a + b) + (c + d)"} there are three positions
     1.7 -  where commutativity of @{text "+"} is applicable: 1 refers to the
     1.8 -  whole term, 2 to @{text "a + b"} and 3 to @{text "c + d"}.
     1.9 +  where commutativity of @{text "+"} is applicable: 1 refers to
    1.10 +  @{text "a + b"}, 2 to the whole term, and 3 to @{text "c + d"}.
    1.11  
    1.12    If the positions in the list @{text "(i \<dots> j)"} are non-overlapping
    1.13    (e.g.\ @{text "(2 3)"} in @{text "(a + b) + (c + d)"}) you may
    1.14 @@ -221,9 +221,11 @@
    1.15    the behaviour of @{text subst} is not specified.
    1.16  
    1.17    \item [@{method subst}~@{text "(asm) (i \<dots> j) eq"}] performs the
    1.18 -  substitutions in the assumptions.  Positions @{text "1 \<dots> i\<^sub>1"}
    1.19 -  refer to assumption 1, positions @{text "i\<^sub>1 + 1 \<dots> i\<^sub>2"}
    1.20 -  to assumption 2, and so on.
    1.21 +  substitutions in the assumptions. The positions refer to the
    1.22 +  assumptions in order from left to right.  For example, given in a
    1.23 +  goal of the form @{text "P (a + b) \<Longrightarrow> P (c + d) \<Longrightarrow> \<dots>"}, position 1 of
    1.24 +  commutativity of @{text "+"} is the subterm @{text "a + b"} and
    1.25 +  position 2 is the subterm @{text "c + d"}.
    1.26  
    1.27    \item [@{method hypsubst}] performs substitution using some
    1.28    assumption; this only works for equations of the form @{text "x =