equal
deleted
inserted
replaced
3 'ig00'; |
3 'ig00'; |
4 # |
4 # |
5 # $Header$ |
5 # $Header$ |
6 # |
6 # |
7 # $Log$ |
7 # $Log$ |
8 # Revision 1.2 1997/03/17 11:25:52 wenzelm |
8 # Revision 1.3 1998/10/19 13:37:02 oheimb |
|
9 # corrected Header |
|
10 # |
|
11 # Revision 1.2 1997/03/17 11:25:52 wenzelm |
9 # fixed perl path; |
12 # fixed perl path; |
10 # |
13 # |
11 # Revision 1.1.1.1 1996/06/25 15:44:59 oheimb |
14 # Revision 1.1.1.1 1996/06/25 15:44:59 oheimb |
12 # Graphical 8bit Font Packet, see isabelle/Tools/8bit/doc/manual.dvi |
15 # Graphical 8bit Font Packet, see isabelle/Tools/8bit/doc/manual.dvi |
13 # Author: Franz Regensburger; improvements by David von Oheimb |
16 # Author: Franz Regensburger; improvements by David von Oheimb |