equal
deleted
inserted
replaced
784 \item[@{text "t."}\hthm{sel\_exhaust} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\ |
784 \item[@{text "t."}\hthm{sel\_exhaust} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\ |
785 @{thm list.sel_exhaust[no_vars]} |
785 @{thm list.sel_exhaust[no_vars]} |
786 |
786 |
787 \item[@{text "t."}\hthm{expand}\rm:] ~ \\ |
787 \item[@{text "t."}\hthm{expand}\rm:] ~ \\ |
788 @{thm list.expand[no_vars]} |
788 @{thm list.expand[no_vars]} |
|
789 |
|
790 \item[@{text "t."}\hthm{sel\_split}\rm:] ~ \\ |
|
791 @{thm list.sel_split[no_vars]} |
|
792 |
|
793 \item[@{text "t."}\hthm{sel\_split\_asm}\rm:] ~ \\ |
|
794 @{thm list.sel_split_asm[no_vars]} |
789 |
795 |
790 \item[@{text "t."}\hthm{case\_conv\_if}\rm:] ~ \\ |
796 \item[@{text "t."}\hthm{case\_conv\_if}\rm:] ~ \\ |
791 @{thm list.case_conv_if[no_vars]} |
797 @{thm list.case_conv_if[no_vars]} |
792 |
798 |
793 \end{description} |
799 \end{description} |