# HG changeset patch
# User desharna
# Date 1413904992 -7200
# Node ID 797d0e7aefc77f78424520b96007c11981e2cab1
# Parent  854eed6e5aed503f88d7c8804ec15d7c4e2bedfa
move documentation of 'rec_o_map'

diff -r 854eed6e5aed -r 797d0e7aefc7 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Tue Oct 21 17:23:11 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Tue Oct 21 17:23:12 2014 +0200
@@ -1021,6 +1021,9 @@
 (The @{text "[code]"} attribute is set by the @{text code} plugin,
 Section~\ref{ssec:code-generator}.)
 
+\item[@{text "t."}\hthm{rec_o_map}\rm:] ~ \\
+@{thm list.rec_o_map[no_vars]}
+
 \item[@{text "t."}\hthm{rec_transfer}\rm:] ~ \\
 @{thm list.rec_transfer[no_vars]}
 
@@ -2860,9 +2863,6 @@
 @{thm list.size(3)[no_vars]} \\
 @{thm list.size(4)[no_vars]}
 
-\item[@{text "t."}\hthm{rec_o_map}\rm:] ~ \\
-@{thm list.rec_o_map[no_vars]}
-
 \item[@{text "t."}\hthm{size_o_map}\rm:] ~ \\
 @{thm list.size_o_map[no_vars]}