equal
deleted
inserted
replaced
929 \item[@{text "t."}\hthm{inj_map_strong}\rm:] ~ \\ |
929 \item[@{text "t."}\hthm{inj_map_strong}\rm:] ~ \\ |
930 @{thm list.inj_map_strong[no_vars]} |
930 @{thm list.inj_map_strong[no_vars]} |
931 |
931 |
932 \item[@{text "t."}\hthm{set_map}\rm:] ~ \\ |
932 \item[@{text "t."}\hthm{set_map}\rm:] ~ \\ |
933 @{thm list.set_map[no_vars]} |
933 @{thm list.set_map[no_vars]} |
|
934 |
|
935 \item[@{text "t."}\hthm{set_transfer}\rm:] ~ \\ |
|
936 @{thm list.set_transfer[no_vars]} |
934 |
937 |
935 \item[@{text "t."}\hthm{map_comg0}\rm:] ~ \\ |
938 \item[@{text "t."}\hthm{map_comg0}\rm:] ~ \\ |
936 @{thm list.map_cong0[no_vars]} |
939 @{thm list.map_cong0[no_vars]} |
937 |
940 |
938 \item[@{text "t."}\hthm{map_cong} @{text "[fundef_cong]"}\rm:] ~ \\ |
941 \item[@{text "t."}\hthm{map_cong} @{text "[fundef_cong]"}\rm:] ~ \\ |