src/Pure/General/scan.ML
Tue, 21 Mar 2006 12:18:17 +0100 wenzelm added ~$$ (negative literal);
Sat, 18 Mar 2006 20:10:50 +0100 wenzelm made $$ and "this" monomorphic (string);
Sat, 14 Jan 2006 17:14:16 +0100 wenzelm Output.error_msg;
Wed, 13 Jul 2005 16:07:24 +0200 wenzelm tuned;
Tue, 21 Jun 2005 09:35:32 +0200 wenzelm tuned;
Wed, 18 May 2005 11:30:59 +0200 wenzelm tuned;
Thu, 07 Apr 2005 09:26:29 +0200 wenzelm added some, peek, trace'; tuned;
Thu, 03 Mar 2005 12:43:01 +0100 skalberg Move towards standard functions.
Sun, 13 Feb 2005 17:15:14 +0100 skalberg Deleted Library.option type.
Mon, 21 Jun 2004 10:25:57 +0200 kleing Merged in license change from Isabelle2004
Wed, 16 Jun 2004 20:37:00 +0200 wenzelm tuned;
Sat, 12 Jun 2004 22:46:39 +0200 wenzelm added trace (inefficient for very long input);
Wed, 09 Jun 2004 18:56:09 +0200 wenzelm added this_string;
Sat, 29 May 2004 15:06:04 +0200 wenzelm Output.error;
Mon, 10 May 2004 19:25:59 +0200 wenzelm added Scan.list;
Thu, 29 Apr 2004 06:03:41 +0200 wenzelm added is_literal;
Mon, 26 Apr 2004 14:58:29 +0200 wenzelm tuned presentation;
Fri, 11 Jul 2003 15:00:54 +0200 berghofe Restored old (tail recursive!) version of repeat.
Sat, 28 Jun 2003 13:42:56 +0200 kleing integrated optimizations by Sebastian Skalberg,
Wed, 29 Jan 2003 17:35:11 +0100 berghofe Some tuning:
Fri, 31 Aug 2001 16:17:52 +0200 berghofe Tuned function extend_lexicon.
Fri, 29 Dec 2000 19:44:13 +0100 wenzelm recover: result;
Sun, 25 Jun 2000 23:46:39 +0200 wenzelm added state: 'a * 'b -> 'a * ('a * 'b);
Fri, 05 May 2000 22:02:46 +0200 wenzelm GPLed;
Sat, 01 Apr 2000 20:15:55 +0200 wenzelm recover: observe stopper;
Fri, 16 Jul 1999 22:25:07 +0200 wenzelm tuned dest_lexicon;
Wed, 12 May 1999 16:52:28 +0200 wenzelm rearranged order of modules;
Wed, 13 Jan 1999 15:18:02 +0100 wenzelm fixed titles;
Wed, 13 Jan 1999 12:44:33 +0100 wenzelm files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
less more (0) tip