| Wed, 06 Jul 2005 10:41:49 +0200 | wenzelm | ThyInfo.time_use root; | changeset | files |
| Wed, 06 Jul 2005 10:41:48 +0200 | wenzelm | added output_buffer; | changeset | files |
| Wed, 06 Jul 2005 10:41:47 +0200 | wenzelm | added write_list, append_list; | changeset | files |
| Wed, 06 Jul 2005 10:41:46 +0200 | wenzelm | tuned write: use File.write_list; | changeset | files |
| Wed, 06 Jul 2005 10:41:45 +0200 | wenzelm | tuned maxidx; | changeset | files |
| Wed, 06 Jul 2005 10:41:44 +0200 | wenzelm | tuned maxidx_of_typ/typs/term; | changeset | files |
| Wed, 06 Jul 2005 10:41:43 +0200 | wenzelm | multiple flags: prefer later ones; | changeset | files |