equal
deleted
inserted
replaced
969 @{thm list.rel_map(1)[no_vars]} \\ |
969 @{thm list.rel_map(1)[no_vars]} \\ |
970 @{thm list.rel_map(2)[no_vars]} |
970 @{thm list.rel_map(2)[no_vars]} |
971 |
971 |
972 \item[@{text "t."}\hthm{rel_mono}\rm:] ~ \\ |
972 \item[@{text "t."}\hthm{rel_mono}\rm:] ~ \\ |
973 @{thm list.rel_mono[no_vars]} |
973 @{thm list.rel_mono[no_vars]} |
|
974 |
|
975 \item[@{text "t."}\hthm{rel_transfer}\rm:] ~ \\ |
|
976 @{thm list.rel_transfer[no_vars]} |
974 |
977 |
975 \end{description} |
978 \end{description} |
976 \end{indentblock} |
979 \end{indentblock} |
977 *} |
980 *} |
978 |
981 |