2008-04-17 wenzelm 2008-04-17 moved default token translations to proof_context.ML, if all fails the pretty printer falls back on plain output;
2008-02-04 wenzelm 2008-02-04 *** MESSAGE REFERS TO 1.29 and 1.44 *** sort_of_term: be permissive about _class *output* markers, to allow print translations invoke this function as well;
2008-02-01 haftmann 2008-02-01 fixed term_of_sort
2007-09-23 wenzelm 2007-09-23 TypeInfer.constrain: canonical argument order;
2007-09-17 wenzelm 2007-09-17 added print_mode_value (CRITICAL);
2007-05-31 wenzelm 2007-05-31 decode_term: force qualified name into Const;
2007-04-21 wenzelm 2007-04-21 TypeExt.decode_term;
2007-04-15 wenzelm 2007-04-15 added decode_types (from type_infer.ML); decode sorts: internalize here; tuned;
2006-10-04 haftmann 2006-10-04 insert replacing ins ins_int ins_string
2006-03-21 wenzelm 2006-03-21 avoid polymorphic equality;
2005-06-29 wenzelm 2005-06-29 export no_type_brackets; accomodate advanced trfuns; tuned;
2005-04-23 wenzelm 2005-04-23 removed token_trans.ML (some content moved to syn_ext.ML);
2005-04-16 wenzelm 2005-04-16 Syntax.mk_trfun;
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-06-09 wenzelm 2004-06-09 removed separate logtypes field of syntax;
2004-05-29 wenzelm 2004-05-29 tuned _dummy_ofsort syntax;
2003-11-06 schirmer 2003-11-06 Records: - Record types are now by default printed with their type abbreviation instead of the list of all field types. This can be configured via the reference "print_record_type_abbr". - Simproc "record_upd_simproc" for simplification of multiple updates added (not enabled by default). - Tactic "record_split_simp_tac" to split and simplify records added. - Bug-fix and optimisation of "record_simproc". - "record_simproc" and "record_upd_simproc" are now sensitive to quick_and_dirty flag.
2003-07-02 nipkow 2003-07-02 Type antiquotations do not use the bracket syntax by default any longer.
2002-01-16 wenzelm 2002-01-16 GPLed;
2001-11-28 wenzelm 2001-11-28 support "_::foo" sort constraints;
2001-05-20 nipkow 2001-05-20 added (no)_type_brackets
2000-12-01 wenzelm 2000-12-01 no_brackets mode;
2000-06-14 wenzelm 2000-06-14 tuned tappl syntax;
2000-05-21 wenzelm 2000-05-21 added sort_of_term; export sortT;
1999-09-07 wenzelm 1999-09-07 logtypes: pretend "dummy" is one;
1999-07-06 wenzelm 1999-07-06 export term_of_typ;
1998-10-20 wenzelm 1998-10-20 no open;
1997-10-10 wenzelm 1997-10-10 added longid syntax;
1997-10-06 wenzelm 1997-10-06 fixed raw_term_sorts (again!); eliminated raise_ast;
1997-02-28 wenzelm 1997-02-28 term_of_... now mark class, tfree, tvar;
1997-02-24 wenzelm 1997-02-24 added "_" syntax for dummyT;
1997-02-06 wenzelm 1997-02-06 improved comments; raw_term_sorts: improved handling of sort constraints (consistency); added term_of_sort; renamed "_emptysort" to "_topsort"; preparations for marking of class idts;
1996-12-18 oheimb 1996-12-18 little improvement for the handling of sort constraints: two non-identical explicit constriants are considered equal if they give the same set in different enumerations, e.g. {term,ord,ord} = {ord,term}
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.
1994-12-08 clasohm 1994-12-08 changed Pure's grammar and the way types are converted to nonterminals
1994-10-12 wenzelm 1994-10-12 removed old comment;
1994-10-04 clasohm 1994-10-04 made major changes to grammar; added call of Type.infer_types to automatically eliminate ambiguities
1994-08-19 wenzelm 1994-08-19 added raw_term_sorts and changed typ_of_term accordingly (part of fix of the typevar-sort-constraint BUG); various minor internal changes;
1994-05-02 wenzelm 1994-05-02 changed translation of type applications according to new grammar;
1994-04-22 clasohm 1994-04-22 changed the way a grammar is generated to allow the new parser to work; also made a lot of changes in parser.ML and minor ones elsewhere
1994-02-03 wenzelm 1994-02-03 minor internal changes;
1994-01-19 wenzelm 1994-01-19 minor internal changes;
1993-10-04 wenzelm 1993-10-04 lots of internal cleaning and tuning; removed {parse,print}_{pre,post}_proc; new lexer: now human readable due to scanner combinators; new parser installed, but still inactive (due to grammar ambiguities); added Syntax.test_read; typ_of_term: sorts now made distinct and sorted; mixfix: added forced line breaks (//); PROP now printed before subterm of type prop with non-const head;
1993-09-16 clasohm 1993-09-16 Initial revision