equal
deleted
inserted
replaced
997 |
997 |
998 \item[@{text "t."}\hthm{rel_mono} @{text "[mono, relator_mono]"}\rm:] ~ \\ |
998 \item[@{text "t."}\hthm{rel_mono} @{text "[mono, relator_mono]"}\rm:] ~ \\ |
999 @{thm list.rel_mono[no_vars]} \\ |
999 @{thm list.rel_mono[no_vars]} \\ |
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 |
|
1003 \item[@{text "t."}\hthm{rel_mono_strong}\rm:] ~ \\ |
|
1004 @{thm list.rel_mono_strong[no_vars]} |
|
1005 |
|
1006 \item[@{text "t."}\hthm{rel_cong} @{text "[fundef_cong]"}\rm:] ~ \\ |
|
1007 @{thm list.rel_cong[no_vars]} |
|
1008 |
|
1009 \item[@{text "t."}\hthm{rel_cong_simp}\rm:] ~ \\ |
|
1010 @{thm list.rel_cong_simp[no_vars]} |
1002 |
1011 |
1003 \item[@{text "t."}\hthm{rel_refl}\rm:] ~ \\ |
1012 \item[@{text "t."}\hthm{rel_refl}\rm:] ~ \\ |
1004 @{thm list.rel_refl[no_vars]} |
1013 @{thm list.rel_refl[no_vars]} |
1005 |
1014 |
1006 \item[@{text "t."}\hthm{rel_refl_strong}\rm:] ~ \\ |
1015 \item[@{text "t."}\hthm{rel_refl_strong}\rm:] ~ \\ |