| changeset 58739 | cf78e16caa3a |
| parent 58737 | b45405874f8f |
| child 58914 | 0ef44616fd5f |
| child 58931 | 3097ec653547 |
--- a/src/Doc/Datatypes/Datatypes.thy Tue Oct 21 17:23:14 2014 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Tue Oct 21 17:23:16 2014 +0200 @@ -2870,8 +2870,8 @@ @{thm list.size_gen(1)[no_vars]} \\ @{thm list.size_gen(2)[no_vars]} -\item[@{text "t."}\hthm{size_o_map}\rm:] ~ \\ -@{thm list.size_o_map[no_vars]} +\item[@{text "t."}\hthm{size_gen_o_map}\rm:] ~ \\ +@{thm list.size_gen_o_map[no_vars]} \end{description} \end{indentblock}