equal
deleted
inserted
replaced
853 \begin{indentblock} |
853 \begin{indentblock} |
854 \begin{description} |
854 \begin{description} |
855 |
855 |
856 \item[@{text "t."}\hthm{case_transfer}\rm:] ~ \\ |
856 \item[@{text "t."}\hthm{case_transfer}\rm:] ~ \\ |
857 @{thm list.case_transfer[no_vars]} |
857 @{thm list.case_transfer[no_vars]} |
|
858 |
|
859 \item[@{text "t."}\hthm{sel_transfer}\rm:] ~ \\ |
|
860 This property is missing for @{typ "'a list"} because there is no common |
|
861 selector to all constructors. |
858 |
862 |
859 \item[@{text "t."}\hthm{ctr_transfer}\rm:] ~ \\ |
863 \item[@{text "t."}\hthm{ctr_transfer}\rm:] ~ \\ |
860 @{thm list.ctr_transfer(1)[no_vars]} \\ |
864 @{thm list.ctr_transfer(1)[no_vars]} \\ |
861 @{thm list.ctr_transfer(2)[no_vars]} |
865 @{thm list.ctr_transfer(2)[no_vars]} |
862 |
866 |