1@Term{term_id_4, 2 label = "a short description of term form external file", 3 force_index, 4 options = "width=20", 5 content = ``SOME_FUN = SUC a < 0 /\ 0 > SUC b`` 6} 7 8@Type{type_id_4, 9 label = "a short description of the type from external file", 10 force_index, 11 short-index, 12 content = ``:bool`` 13} 14 15 16@Thm{arithmetic.LESS_SUC_EQ_COR, 17 force-index, 18 long-index, 19 latex = "My latex code for \texttt{LESS_SUC_EQ_COR}" 20} 21 22@Thm{arithmetic.LESS_EQ_0, 23 force-index, long-index 24} 25 26@Thm{thm_1, 27 label = "(second instance)", 28 content = "arithmetic.LESS_SUC_EQ_COR", 29 options = "width=20", 30 comment = "some lengthy\\comment 31 32 with \textbf{formats} and newlines", 33 force-index, 34 long-index 35} 36 37@Theorems{ 38 ids = [arithmetic.LESS_ADD_SUC, 39 arithmetic.LESS_EQ*], 40 force-index 41} 42 43