author | desharna |
Tue, 21 Oct 2014 17:23:16 +0200 | |
changeset 58739 | cf78e16caa3a |
parent 58738 | 2af42aecc120 |
child 58740 | cb9d84d3e7f2 |
--- 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}