src/Pure/Syntax/mixfix.ML
2005-10-07 wenzelm 2005-10-07 added syntax for _idtdummy, _idtypdummy; removed obsolete _K;
2005-09-06 wenzelm 2005-09-06 deprecated old-style infix declarations, which mix name and syntax;
2005-06-29 wenzelm 2005-06-29 accomodate advanced trfuns;
2005-04-16 wenzelm 2005-04-16 identify binder translations only once (admits remove);
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-09 wenzelm 2004-06-09 removed separate logtypes field of syntax;
2004-06-01 wenzelm 2004-06-01 removed obsolete sort 'logic' and '=?=' syntax;
2004-05-29 wenzelm 2004-05-29 \<^bsub>/\<^esub> syntax: unbreakable block;
2004-05-01 wenzelm 2004-05-01 improved indexed syntax / implicit structures;
2004-04-23 wenzelm 2004-04-23 index syntax: support for general expressions (input only);
2004-04-22 wenzelm 2004-04-22 non_typed_tr';
2004-01-27 nipkow 2004-01-27 Reduced space for xsymbols output of [| |] ==> from 3 to 1
2002-01-30 wenzelm 2002-01-30 added literal;
2002-01-16 wenzelm 2002-01-16 GPLed;
2001-12-18 wenzelm 2001-12-18 improved mixfix_args;
2001-12-14 wenzelm 2001-12-14 removed special treatment of "_" in syntax (now covered by \<index> arg);
2001-11-11 wenzelm 2001-11-11 pure_syntax_output: "_meta_conjunction";
2001-11-09 wenzelm 2001-11-09 removed pure_sym_syntax; allow additional arguments in infixes (maximum priority);
2001-11-08 wenzelm 2001-11-08 proper syntax for structs;
2001-11-07 wenzelm 2001-11-07 syntax for structs;
2001-10-28 wenzelm 2001-10-28 fixed string_of_mixfix;
2001-10-24 wenzelm 2001-10-24 added string_of_mixfix;
2001-10-02 wenzelm 2001-10-02 support non-oriented infix;
2001-02-11 wenzelm 2001-02-11 added "xsymbols" syntax for "=?=";
2000-08-29 wenzelm 2000-08-29 added \<dots> syntax;
1999-09-04 wenzelm 1999-09-04 removed "_BIND" syntax;
1999-07-08 wenzelm 1999-07-08 aprop: ??id, ...;
1999-06-02 wenzelm 1999-06-02 "..." syntax;
1999-04-14 wenzelm 1999-04-14 fixed named type infixes (actual BUG!);
1998-12-11 oheimb 1998-12-11 added new print_mode "xsymbols" for extended symbol support (e.g. genuiely long arrows)
1998-10-20 wenzelm 1998-10-20 no open;
1998-08-10 wenzelm 1998-08-10 ??id syntax for text variables;
1998-06-20 wenzelm 1998-06-20 added fix_mixfix;
1998-05-13 wenzelm 1998-05-13 pure_nonterms;
1998-04-22 wenzelm 1998-04-22 added no_syn;
1998-03-09 wenzelm 1998-03-09 Symbol.explode;
1997-11-05 wenzelm 1997-11-05 added TYPE syntax; tuned;
1997-10-31 wenzelm 1997-10-31 added mixfix_args;
1997-10-10 wenzelm 1997-10-10 added longid syntax;
1997-10-09 wenzelm 1997-10-09 fixed infix syntax;
1997-09-22 wenzelm 1997-09-22 fixed idt/idts vs. pttrn/pttrns;
1997-04-24 oheimb 1997-04-24 changed priority of '%': now no parenteses needed for '[...] == %x. [...]'
1997-03-07 wenzelm 1997-03-07 added \<Colon> syntax for constraints (more compact!);
1997-02-28 wenzelm 1997-02-28 added _mk_ofclass(S);
1997-02-21 wenzelm 1997-02-21 declared the dummy type;
1997-02-21 wenzelm 1997-02-21 tuned symbolic [|_|] syntax;
1996-12-13 wenzelm 1996-12-13 binder_tr': applied fix_tr';
1996-11-27 wenzelm 1996-11-27 symbol name changes;
1996-11-18 wenzelm 1996-11-18 added Infixl/rName: specify infix name independently from syntax; added Pure symbolfont syntax;
1996-09-05 paulson 1996-09-05 Pretty-printing change to emphasize the scope of assumptions
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-07-07 clasohm 1995-07-07 moved mixfix syntax from sign.ML
1995-07-03 clasohm 1995-07-03 added cargs for curried function application
1995-04-22 nipkow 1995-04-22 I have modified the grammar for idts (sequences of identifiers with optional type annotations). idts are generally used as in abstractions, be it lambda-abstraction or quantifiers. It now has roughly the form idts = pttrn* pttrn = idt where pttrn is a new nonterminal (type) not used anywhere else. This means that the Pure syntax for idts is in fact unchanged. The point is that the new nontermianl pttrn allows later extensions of this syntax. (See, for example, HOL/Prod.thy). The name idts is not quite accurate any longer and may become downright confusing once pttrn has been extended. Something should be done about this, in particular wrt to the manual.
1995-03-03 clasohm 1995-03-03 added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
1995-03-02 wenzelm 1995-03-02 added declaration of syntactic const "_abs";
1995-01-27 wenzelm 1995-01-27 *** empty log message ***