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