minor doc fix (there is no guarantee that the equations for a given f_i are contiguous in the collection)
authorblanchet
Wed Oct 02 10:34:13 2013 +0200 (2013-10-02)
changeset 54023cede3c1d2417
parent 54022 aae0163c01ea
child 54024 07ab4fd922c2
minor doc fix (there is no guarantee that the equations for a given f_i are contiguous in the collection)
src/Doc/Datatypes/Datatypes.thy
     1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Wed Oct 02 10:15:53 2013 +0300
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Wed Oct 02 10:34:13 2013 +0200
     1.3 @@ -1329,8 +1329,8 @@
     1.4  
     1.5  \item \emph{Theorems sometimes have different names.}
     1.6  For $m > 1$ mutually recursive functions,
     1.7 -@{text "f\<^sub>1_\<dots>_f\<^sub>m.simps(k\<^sub>i,\<dots>,k\<^sub>i+n\<^sub>i-1)"} have
     1.8 -been renamed @{text "f\<^sub>i.simps(1,\<dots>,n\<^sub>i-1)"}.
     1.9 +@{text "f\<^sub>1_\<dots>_f\<^sub>m.simps"} has been broken down into separate
    1.10 +subcollections @{text "f\<^sub>i.simps"}.
    1.11  \end{itemize}
    1.12  *}
    1.13