author | desharna |
Wed, 02 Jul 2014 17:01:51 +0200 | |
changeset 57490 | afc7081f19d4 |
parent 57489 | 8f0ba9f2d10f |
child 57491 | 9eedaafc05c8 |
--- a/src/Doc/Datatypes/Datatypes.thy Wed Jul 02 17:01:49 2014 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Wed Jul 02 17:01:51 2014 +0200 @@ -1766,6 +1766,9 @@ @{thm llist.corec(1)[no_vars]} \\ @{thm llist.corec(2)[no_vars]} +\item[@{text "t."}\hthm{corec\_code} @{text "[code]"}\rm:] ~ \\ +@{thm llist.corec_code[no_vars]} + \item[@{text "t."}\hthm{disc\_corec}\rm:] ~ \\ @{thm llist.disc_corec(1)[no_vars]} \\ @{thm llist.disc_corec(2)[no_vars]}