equal
deleted
inserted
replaced
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 |