src/Pure/Syntax/syn_trans.ML
2006-12-10 wenzelm 2006-12-10 abs/binder_tr': support printing of idtdummy;
2006-11-26 wenzelm 2006-11-26 tuned;
2006-07-25 wenzelm 2006-07-25 added variant_abs (from term.ML); tuned;
2006-07-18 wenzelm 2006-07-18 Term.declare_term_names;
2006-07-11 wenzelm 2006-07-11 Name.invent_list;
2006-06-11 wenzelm 2006-06-11 improved treatment of TERM TYPE syntax;
2006-05-05 wenzelm 2006-05-05 added syntax for _type_constraint_;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-04-26 wenzelm 2006-04-26 tuned;
2006-03-21 wenzelm 2006-03-21 mark_boundT: produce well-typed term;
2006-02-23 wenzelm 2006-02-23 make SML/NJ happy;
2006-02-22 wenzelm 2006-02-22 removed obsolete meta_conjunction_tr';
2006-02-10 wenzelm 2006-02-10 moved fixedN to lexicon.ML; tuned;
2006-02-06 wenzelm 2006-02-06 added bound_vars;
2006-01-31 wenzelm 2006-01-31 advanced translations: Context.generic;
2006-01-14 wenzelm 2006-01-14 sane ERROR handling;
2005-12-22 wenzelm 2005-12-22 prop_tr': proper handling of aprop marked as bound;
2005-12-02 wenzelm 2005-12-02 asts_to_terms: builtin free_fixed translation makes local binders work properly;
2005-11-19 wenzelm 2005-11-19 tuned;
2005-11-09 wenzelm 2005-11-09 tuned;
2005-10-07 wenzelm 2005-10-07 added idtypdummy_ast_tr; removed obsolete k_tr;
2005-09-13 wenzelm 2005-09-13 replaced TRANSLATION_FAIL by EXCEPTION;
2005-06-29 wenzelm 2005-06-29 transform_failure in translation functions: TRANSLATION_FAIL; proper treatment of advanced trfuns: pass thy argument; tuned bigimpl_ast_tr, impl_ast_tr';
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-12-18 schirmer 2004-12-18 Syntax: last premise of "_bigimpl" is wrapped with "_asm", to have a hook for printing.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-06-05 wenzelm 2004-06-05 tuned exeption handling (capture/release);
2004-05-21 berghofe 2004-05-21 Modified functions pt_to_ast and ast_to_term to improve handling of errors in parse (ast) translations caused by ambiguous input.
2004-05-01 wenzelm 2004-05-01 improved indexed syntax / implicit structures;
2004-04-22 wenzelm 2004-04-22 non_typed_tr';
2002-12-22 nipkow 2002-12-22 *** empty log message ***
2002-01-16 wenzelm 2002-01-16 GPLed;
2001-11-11 wenzelm 2001-11-11 added meta_conjunction_tr';
2001-11-09 wenzelm 2001-11-09 indexvar_ast_tr (for \<index> placeholder);
2001-08-08 wenzelm 2001-08-08 added constify_ast_tr;
2000-12-01 wenzelm 2000-12-01 no_brackets mode;
2000-03-27 wenzelm 2000-03-27 fixed dddot_tr;
2000-03-25 wenzelm 2000-03-25 improved (anti)quote_tr(');
2000-03-25 wenzelm 2000-03-25 tuned antiquote_tr';
2000-03-23 wenzelm 2000-03-23 tuned spacing;
1999-09-04 wenzelm 1999-09-04 removed "_BIND" translation;
1999-06-02 wenzelm 1999-06-02 added dddot_tr;
1998-10-20 wenzelm 1998-10-20 no open;
1998-08-10 wenzelm 1998-08-10 tuned;
1998-06-25 wenzelm 1998-06-25 tuned loose bound vars check; added quote_antiquote_tr(');
1998-03-09 wenzelm 1998-03-09 read_var;
1997-11-05 wenzelm 1997-11-05 adapted pure_trfunsT; added type_tr/tr'; eliminated mk_ofclassS_tr';
1997-10-17 wenzelm 1997-10-17 no longer tries bogus eta-contract involving aprops;
1997-10-06 wenzelm 1997-10-06 eliminated raise_ast, raise_term, raise_typ;
1997-09-24 wenzelm 1997-09-24 pure_trfuns: added constraint;
1997-09-22 wenzelm 1997-09-22 tuned lambda_ast_tr, idtyp_ast_tr' to accomodate fix of idt/idts vs. pttrn/pttrns;
1997-02-28 wenzelm 1997-02-28 added mark_bound(T), variant_abs'; trfuns now mark bounds they introduce!! added pure_trfunsT;
1996-02-16 paulson 1996-02-16 Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
1995-11-12 nipkow 1995-11-12 Set eta_contract to true.
1995-07-03 clasohm 1995-07-03 added cargs for curried function application
1995-03-30 clasohm 1995-03-30 changed translation of _applC
1995-03-03 clasohm 1995-03-03 added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
1994-10-12 wenzelm 1994-10-12 remove _explode, _implode and trfuns;
1994-09-26 wenzelm 1994-09-26 explode_tr now produces leadings 0s; implode_ast_tr' now quotes result;