Wed, 14 May 2008 11:05:11 +0200 | wenzelm | use_text/file: proper position output; | changeset | files |
Wed, 14 May 2008 11:05:10 +0200 | wenzelm | renamed Position.path to Path.position; | changeset | files |
Wed, 14 May 2008 11:05:08 +0200 | wenzelm | renamed Position.path to Path.position; | changeset | files |
Wed, 14 May 2008 11:05:07 +0200 | wenzelm | load seq.ML and position.ML earlier; | changeset | files |