equal
deleted
inserted
replaced
1000 The @{text "[relator_mono]"} attribute is set by the @{text lifting} plugin |
1000 The @{text "[relator_mono]"} attribute is set by the @{text lifting} plugin |
1001 (Section~\ref{ssec:lifting}). |
1001 (Section~\ref{ssec:lifting}). |
1002 |
1002 |
1003 \item[@{text "t."}\hthm{rel_refl}\rm:] ~ \\ |
1003 \item[@{text "t."}\hthm{rel_refl}\rm:] ~ \\ |
1004 @{thm list.rel_refl[no_vars]} |
1004 @{thm list.rel_refl[no_vars]} |
|
1005 |
|
1006 \item[@{text "t."}\hthm{rel_refl_strong}\rm:] ~ \\ |
|
1007 @{thm list.rel_refl_strong[no_vars]} |
|
1008 |
|
1009 \item[@{text "t."}\hthm{rel_reflp}\rm:] ~ \\ |
|
1010 @{thm list.rel_reflp[no_vars]} |
|
1011 |
|
1012 \item[@{text "t."}\hthm{rel_symp}\rm:] ~ \\ |
|
1013 @{thm list.rel_symp[no_vars]} |
|
1014 |
|
1015 \item[@{text "t."}\hthm{rel_transp}\rm:] ~ \\ |
|
1016 @{thm list.rel_transp[no_vars]} |
1005 |
1017 |
1006 \item[@{text "t."}\hthm{rel_transfer} @{text "[transfer_rule]"}\rm:] ~ \\ |
1018 \item[@{text "t."}\hthm{rel_transfer} @{text "[transfer_rule]"}\rm:] ~ \\ |
1007 @{thm list.rel_transfer[no_vars]} \\ |
1019 @{thm list.rel_transfer[no_vars]} \\ |
1008 The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin |
1020 The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin |
1009 (Section~\ref{ssec:transfer}) for type constructors with no dead type arguments. |
1021 (Section~\ref{ssec:transfer}) for type constructors with no dead type arguments. |