equal
deleted
inserted
replaced
23 \isanewline |
23 \isanewline |
24 % |
24 % |
25 \endisadeliminvisible |
25 \endisadeliminvisible |
26 % |
26 % |
27 \isataginvisible |
27 \isataginvisible |
28 \isacommand{hide}\isamarkupfalse% |
28 \isacommand{hide{\isacharunderscore}const}\isamarkupfalse% |
29 \ const\ Lattices{\isachardot}lattice\isanewline |
29 \ Lattices{\isachardot}lattice\isanewline |
30 \isacommand{pretty{\isacharunderscore}setmargin}\isamarkupfalse% |
30 \isacommand{pretty{\isacharunderscore}setmargin}\isamarkupfalse% |
31 \ {\isadigit{6}}{\isadigit{5}}% |
31 \ {\isadigit{6}}{\isadigit{5}}% |
32 \endisataginvisible |
32 \endisataginvisible |
33 {\isafoldinvisible}% |
33 {\isafoldinvisible}% |
34 % |
34 % |