equal
deleted
inserted
replaced
784 \item[@{text "t."}\hthm{case\_conv\_if}\rm:] ~ \\ |
784 \item[@{text "t."}\hthm{case\_conv\_if}\rm:] ~ \\ |
785 @{thm list.case_conv_if[no_vars]} |
785 @{thm list.case_conv_if[no_vars]} |
786 |
786 |
787 \end{description} |
787 \end{description} |
788 \end{indentblock} |
788 \end{indentblock} |
|
789 |
|
790 \noindent |
|
791 In addition, equational versions of @{text t.disc} are registered with the @{text "[code]"} |
|
792 attribute. |
789 *} |
793 *} |
790 |
794 |
791 |
795 |
792 subsubsection {* Functorial Theorems |
796 subsubsection {* Functorial Theorems |
793 \label{sssec:functorial-theorems} *} |
797 \label{sssec:functorial-theorems} *} |