lib/scripts/symbolinput.pl
Tue, 29 Apr 1997 17:38:02 +0200 wenzelm deactivated new symbols (not yet printable on xterm, emacs);
Tue, 29 Apr 1997 17:23:53 +0200 wenzelm renamed \<choice> to \<orelse>;
Tue, 29 Apr 1997 16:39:13 +0200 wenzelm added new chars;
Wed, 16 Apr 1997 18:53:36 +0200 wenzelm removed lceil, rceil, lfloor, rfloor;
Sun, 13 Apr 1997 19:15:07 +0200 wenzelm GENERATED TEXT;
Sun, 13 Apr 1997 19:11:32 +0200 wenzelm GENERATED TEXT;
Fri, 07 Mar 1997 15:32:16 +0100 wenzelm removed lparr, rparr, empty, succeq, ge, rrightarrow;
Fri, 21 Feb 1997 16:35:49 +0100 wenzelm replaced natural by subset;
Mon, 16 Dec 1996 16:06:56 +0100 wenzelm fixed Title;
Mon, 16 Dec 1996 15:45:02 +0100 oheimb added consistency comment
Mon, 16 Dec 1996 09:57:18 +0100 wenzelm renamed from symbol_input.pl;
less more (0) tip