Wed, 14 May 2008 20:30:53 +0200 | wenzelm | added defined_command, defined_option; | changeset | files |
Wed, 14 May 2008 20:30:29 +0200 | wenzelm | added intern, defined; | changeset | files |
Wed, 14 May 2008 20:30:05 +0200 | wenzelm | added defined; | changeset | files |
Wed, 14 May 2008 14:43:38 +0200 | wenzelm | setmp_thread_data: do nothing if Output.debugging; | changeset | files |
Wed, 14 May 2008 14:43:37 +0200 | wenzelm | names_of: exclude intermediate ids -- less verbosity; | changeset | files |
Wed, 14 May 2008 14:43:34 +0200 | wenzelm | remobed obsolete keyword concl; | changeset | files |