| Tue, 29 Aug 2000 20:13:17 +0200 | wenzelm | added indent; | file | diff | annotate |
| Sun, 25 Jun 2000 23:46:22 +0200 | wenzelm | fbrk: 2 if not taken; | file | diff | annotate |
| Fri, 05 May 2000 22:02:46 +0200 | wenzelm | GPLed; | file | diff | annotate |
| Wed, 15 Mar 2000 18:18:12 +0100 | wenzelm | removed lst, strlen, strlen_real, spc, sym; | file | diff | annotate |
| Tue, 09 Mar 1999 12:11:00 +0100 | wenzelm | added strlen_real, setmp_margin; | file | diff | annotate |
| Thu, 11 Feb 1999 21:15:46 +0100 | wenzelm | sym: Symbol.output_width; | file | diff | annotate |
| Wed, 13 Jan 1999 15:18:02 +0100 | wenzelm | fixed titles; | file | diff | annotate |
| Wed, 13 Jan 1999 12:44:33 +0100 | wenzelm | files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General; | file | diff | annotate |