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 ***
1995-01-18 clasohm 1995-01-18 added optional precedence for body of binder; removed call to infer_types from read_xrules
1995-01-11 wenzelm 1995-01-11 slightly changed OFCLASS syntax;
1994-12-14 wenzelm 1994-12-14 added any, sprop to pure_types;
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 remove _explode, _implode and trfuns;
1994-10-08 clasohm 1994-10-08 changed precedences of _constrain (i.e. "::")
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 minor cleanings;
1994-07-14 wenzelm 1994-07-14 changed syntax "(| _ : _ |)" to "OFCLASS(_, _)";
1994-05-19 wenzelm 1994-05-19 support for new style mixfix annotations; part of the pure syntax as mixfix (supports axclasses);