| changeset 54624 | 36301c99ed26 |
| parent 54621 | 82a78bc9fa0d |
| child 54626 | 8a5e82425e55 |
--- a/src/Doc/Datatypes/Datatypes.thy Mon Dec 02 20:31:54 2013 +0100 +++ b/src/Doc/Datatypes/Datatypes.thy Mon Dec 02 20:31:54 2013 +0100 @@ -866,7 +866,7 @@ \item[@{text "t."}\hthm{map\_comp}\rm:] ~ \\ @{thm list.map_cong0[no_vars]} -\item[@{text "t."}\hthm{map\_cong} @{text "[cong, fundef_cong]"}\rm:] ~ \\ +\item[@{text "t."}\hthm{map\_cong} @{text "[fundef_cong]"}\rm:] ~ \\ @{thm list.map_cong[no_vars]} \item[@{text "t."}\hthm{map\_id}\rm:] ~ \\