| changeset 53805 | 4163160853fd |
| parent 53798 | 6a4e3299dfd1 |
| child 53822 | 6304b12c7627 |
--- a/src/Doc/Datatypes/Datatypes.thy Mon Sep 23 14:53:43 2013 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Mon Sep 23 17:43:23 2013 +0200 @@ -764,7 +764,7 @@ @{thm list.discI(1)[no_vars]} \\ @{thm list.discI(2)[no_vars]} -\item[@{text "t."}\hthm{sel} @{text "[simp]"}\rm:] ~ \\ +\item[@{text "t."}\hthm{sel} @{text "[simp, code]"}\rm:] ~ \\ @{thm list.sel(1)[no_vars]} \\ @{thm list.sel(2)[no_vars]}