src/Pure/Syntax/syn_trans.ML
2010-05-31 ago modernized some structure names, keeping a few legacy aliases;
2010-04-29 ago uniform decoding of fixed/const syntax entities, allows to pass "\<^fixed>foo__" through the syntax layer (supersedes 1b7109c10b7b);
2010-03-03 ago authentic syntax for classes and type constructors;
2010-02-21 ago authentic syntax for *all* term constants;
2010-02-18 ago made SML/NJ happy (again);
2010-02-16 ago moved generic update_name to Pure syntax -- not specific to HOL/record;
2009-09-30 ago eliminated dead code;
2009-09-29 ago explicit indication of Unsynchronized.ref;
2009-07-21 ago attempt for more concise setup of non-etacontracting binders
2009-06-10 ago reraise exceptions to preserve position information;
2009-02-27 ago eliminated NJ's List.nth;
2008-12-31 ago qualified Term.rename_wrt_term;
2008-11-20 ago Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
2008-10-16 ago added translations for SORT_CONSTRAINT
2008-03-27 ago eliminated theory ProtoPure;
2007-07-24 ago moved exception capture/release to structure Exn;
2007-07-23 ago eliminated transform_failure (to avoid critical section for main transactions);
2007-07-17 ago moved print_translations from Pure.thy to Syntax/syn_trans.ML;
2006-12-11 ago advanced translation functions: Proof.context;
2006-12-10 ago abs/binder_tr': support printing of idtdummy;
2006-11-26 ago tuned;
2006-07-25 ago added variant_abs (from term.ML);
2006-07-18 ago Term.declare_term_names;
2006-07-11 ago Name.invent_list;
2006-06-11 ago improved treatment of TERM TYPE syntax;
2006-05-05 ago added syntax for _type_constraint_;
2006-04-27 ago tuned basic list operators (flat, maps, map_filter);
2006-04-26 ago tuned;
2006-03-21 ago mark_boundT: produce well-typed term;
2006-02-23 ago make SML/NJ happy;
2006-02-22 ago removed obsolete meta_conjunction_tr';
2006-02-10 ago moved fixedN to lexicon.ML;
2006-02-06 ago added bound_vars;
2006-01-31 ago advanced translations: Context.generic;
2006-01-14 ago sane ERROR handling;
2005-12-22 ago prop_tr': proper handling of aprop marked as bound;
2005-12-02 ago asts_to_terms: builtin free_fixed translation makes local binders work properly;
2005-11-19 ago tuned;
2005-11-09 ago tuned;
2005-10-07 ago added idtypdummy_ast_tr;
2005-09-13 ago replaced TRANSLATION_FAIL by EXCEPTION;
2005-06-29 ago transform_failure in translation functions: TRANSLATION_FAIL;
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2004-12-18 ago Syntax: last premise of "_bigimpl" is wrapped with "_asm", to have a hook for
2004-06-21 ago Merged in license change from Isabelle2004
2004-06-05 ago tuned exeption handling (capture/release);
2004-05-21 ago Modified functions pt_to_ast and ast_to_term to improve handling
2004-05-01 ago improved indexed syntax / implicit structures;
2004-04-22 ago non_typed_tr';
2002-12-22 ago *** empty log message ***
2002-01-16 ago GPLed;
2001-11-11 ago added meta_conjunction_tr';
2001-11-09 ago indexvar_ast_tr (for \<index> placeholder);
2001-08-08 ago added constify_ast_tr;
2000-12-01 ago no_brackets mode;
2000-03-27 ago fixed dddot_tr;
2000-03-25 ago improved (anti)quote_tr(');
2000-03-25 ago tuned antiquote_tr';
2000-03-23 ago tuned spacing;