src/HOL/Import/import_syntax.ML
2010-05-28 ago made SML/NJ quite happy;
2010-05-17 ago prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
2010-05-17 ago renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
2009-10-29 ago standardized filter/filter_out;
2009-10-17 ago eliminated hard tabulators, guessing at each author's individual tab-width;
2009-09-29 ago explicit indication of Unsynchronized.ref;
2008-08-12 ago Symbol.source/OuterLex.source: more explicit do_recover argument;
2008-08-07 ago Position.start;
2008-06-25 ago moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
2007-10-06 ago simplified interfaces for outer syntax;
2007-09-25 ago proper Sign operations instead of Theory aliases;
2007-09-25 ago Syntax.parse/check/read;
2007-09-15 ago removed redundant OuterLex.make_lexicon;
2007-07-09 ago adapted OuterLex/T.source;
2007-04-14 ago cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
2007-04-04 ago removed obsolete sign_of/sign_of_thm;
2006-02-15 ago fixed bugs, added caching
2005-09-26 ago fixed disambiguation problem
2005-09-13 ago global quick_and_dirty;
2005-08-16 ago OuterKeyword;
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2004-04-19 ago Forgot a couple of checks for the quick_and_dirty flag the other day.
2004-04-17 ago Minor cleanup of headers and some speedup of the HOL4 import.
2004-04-04 ago Added a number of explicit type casts and delayed evaluations (all seemingly
2004-04-02 ago Added HOL proof importer.