equal
deleted
inserted
replaced
855 \begin{description} |
855 \begin{description} |
856 |
856 |
857 \item[@{text "t."}\hthm{set} @{text "[simp, code]"}\rm:] ~ \\ |
857 \item[@{text "t."}\hthm{set} @{text "[simp, code]"}\rm:] ~ \\ |
858 @{thm list.set(1)[no_vars]} \\ |
858 @{thm list.set(1)[no_vars]} \\ |
859 @{thm list.set(2)[no_vars]} |
859 @{thm list.set(2)[no_vars]} |
|
860 |
|
861 \item[@{text "t."}\hthm{set_cases}\rm:] ~ \\ |
|
862 @{thm list.set_cases[no_vars]} |
860 |
863 |
861 \item[@{text "t."}\hthm{set_empty}\rm:] ~ \\ |
864 \item[@{text "t."}\hthm{set_empty}\rm:] ~ \\ |
862 @{thm list.set_empty[no_vars]} |
865 @{thm list.set_empty[no_vars]} |
863 |
866 |
864 \item[@{text "t."}\hthm{set_intros}\rm:] ~ \\ |
867 \item[@{text "t."}\hthm{set_intros}\rm:] ~ \\ |