equal
deleted
inserted
replaced
887 @{thm list.rel_intros(2)[no_vars]} |
887 @{thm list.rel_intros(2)[no_vars]} |
888 |
888 |
889 % FIXME (and add @ before antiquotation below) |
889 % FIXME (and add @ before antiquotation below) |
890 %\item[@{text "t."}\hthm{rel_cases} @{text "[consumes 1, case_names t\<^sub>1 \<dots> t\<^sub>m, cases pred]"}\rm:] ~ \\ |
890 %\item[@{text "t."}\hthm{rel_cases} @{text "[consumes 1, case_names t\<^sub>1 \<dots> t\<^sub>m, cases pred]"}\rm:] ~ \\ |
891 %{thm list.rel_cases[no_vars]} |
891 %{thm list.rel_cases[no_vars]} |
|
892 |
|
893 \item[@{text "t."}\hthm{rel_sel}\rm:] ~ \\ |
|
894 @{thm list.rel_sel[no_vars]} |
892 |
895 |
893 \end{description} |
896 \end{description} |
894 \end{indentblock} |
897 \end{indentblock} |
895 |
898 |
896 \noindent |
899 \noindent |