equal
deleted
inserted
replaced
884 \item[@{text "t."}\hthm{map\_cong} @{text "[fundef_cong]"}\rm:] ~ \\ |
884 \item[@{text "t."}\hthm{map\_cong} @{text "[fundef_cong]"}\rm:] ~ \\ |
885 @{thm list.map_cong[no_vars]} |
885 @{thm list.map_cong[no_vars]} |
886 |
886 |
887 \item[@{text "t."}\hthm{map\_id}\rm:] ~ \\ |
887 \item[@{text "t."}\hthm{map\_id}\rm:] ~ \\ |
888 @{thm list.map_id[no_vars]} |
888 @{thm list.map_id[no_vars]} |
|
889 |
|
890 \item[@{text "t."}\hthm{map\_id0}\rm:] ~ \\ |
|
891 @{thm list.map_id0[no_vars]} |
889 |
892 |
890 \item[@{text "t."}\hthm{map\_ident}\rm:] ~ \\ |
893 \item[@{text "t."}\hthm{map\_ident}\rm:] ~ \\ |
891 @{thm list.map_ident[no_vars]} |
894 @{thm list.map_ident[no_vars]} |
892 |
895 |
893 \item[@{text "t."}\hthm{rel\_compp}\rm:] ~ \\ |
896 \item[@{text "t."}\hthm{rel\_compp}\rm:] ~ \\ |