changeset 22999 | c1ce129e6f9c |
parent 22657 | 731622340817 |
child 23191 | b7f3a30f3d7f |
22998:97e1f9c2cc46 | 22999:c1ce129e6f9c |
---|---|
77 no_document use_thy "Word"; |
77 no_document use_thy "Word"; |
78 time_use_thy "Adder"; |
78 time_use_thy "Adder"; |
79 |
79 |
80 HTML.with_charset "utf-8" (no_document time_use_thy) "Hebrew"; |
80 HTML.with_charset "utf-8" (no_document time_use_thy) "Hebrew"; |
81 HTML.with_charset "utf-8" (no_document time_use_thy) "Chinese"; |
81 HTML.with_charset "utf-8" (no_document time_use_thy) "Chinese"; |
82 |
|
83 time_use_thy "Unification"; |