src/Doc/Datatypes/Datatypes.thy
changeset 58739 cf78e16caa3a
parent 58737 b45405874f8f
child 58914 0ef44616fd5f
child 58931 3097ec653547
equal deleted inserted replaced
58738:2af42aecc120 58739:cf78e16caa3a
  2868 
  2868 
  2869 \item[@{text "t."}\hthm{size_gen}\rm:] ~ \\
  2869 \item[@{text "t."}\hthm{size_gen}\rm:] ~ \\
  2870 @{thm list.size_gen(1)[no_vars]} \\
  2870 @{thm list.size_gen(1)[no_vars]} \\
  2871 @{thm list.size_gen(2)[no_vars]}
  2871 @{thm list.size_gen(2)[no_vars]}
  2872 
  2872 
  2873 \item[@{text "t."}\hthm{size_o_map}\rm:] ~ \\
  2873 \item[@{text "t."}\hthm{size_gen_o_map}\rm:] ~ \\
  2874 @{thm list.size_o_map[no_vars]}
  2874 @{thm list.size_gen_o_map[no_vars]}
  2875 
  2875 
  2876 \end{description}
  2876 \end{description}
  2877 \end{indentblock}
  2877 \end{indentblock}
  2878 *}
  2878 *}
  2879 
  2879