src/HOL/Set.thy
2000-10-03 wenzelm 2000-10-03 range declared as syntax;
2000-09-28 wenzelm 2000-09-28 fixed \<Union>, \<Inter> syntax;
2000-01-28 oheimb 2000-01-28 beautified spacing for binders with symbols syntax, analogous to HOL.thy
1999-11-11 paulson 1999-11-11 new-style infix declaration for "image"
1999-08-26 paulson 1999-08-26 a little tidying; also FIXED BAD TYPE in INTER1, UNION1
1999-08-17 wenzelm 1999-08-17 replaced HOL_quantifiers flag by "HOL" print mode; simplified HOL basic syntax (more orthogonal);
1998-11-18 paulson 1998-11-18 Finally removing "Compl" from HOL
1998-10-30 paulson 1998-10-30 Moved "instance set:...{power} from Set.thy to RelPow.thy, where is is needed
1998-09-15 paulson 1998-09-15 From Compl(A) to -A
1998-08-05 paulson 1998-08-05 Removal of "disjoint" translation
1998-08-04 wenzelm 1998-08-04 fixed disjount translation;
1998-07-15 nipkow 1998-07-15 Minor tidying up.
1998-03-30 oheimb 1998-03-30 added caveat
1997-11-05 paulson 1997-11-05 UNIV now a constant; UNION1, INTER1 now translations and no longer have separate rules for themselves
1997-11-05 wenzelm 1997-11-05 adapted typed_print_translation;
1997-10-20 wenzelm 1997-10-20 adapted to qualified names;
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-10-09 wenzelm 1997-10-09 fixed infix syntax;
1997-05-30 paulson 1997-05-30 Overloading of "^" requires new type class "power", with types "nat" and "set" in that class. The operator itself is declared in Nat.thy
1997-05-16 nipkow 1997-05-16 Distributed Psubset stuff to basic set theory files, incl Finite. Added stuff by bu.
1997-04-16 wenzelm 1997-04-16 improved translations for subset symbols syntax: constraints;
1997-04-04 nipkow 1997-04-04 moved inj and surj from Set to Fun and Inv -> inv.
1997-02-25 wenzelm 1997-02-25 added proper subset symbols syntax;
1996-12-16 wenzelm 1996-12-16 fixed \<subseteq> input;
1996-12-13 oheimb 1996-12-13 adaptions for symbol font
1996-12-13 wenzelm 1996-12-13 added set inclusion symbol syntax;
1996-12-10 wenzelm 1996-12-10 fixed alternative quantifier symbol syntax;
1996-12-10 wenzelm 1996-12-10 fixed pris of binder syntax;
1996-11-27 wenzelm 1996-11-27 added "op :", "op ~:" syntax; added symbols syntax;
1996-09-23 paulson 1996-09-23 New infix syntax: breaks line BEFORE operator
1996-09-09 paulson 1996-09-09 Corrected associativity: must be to right, as the type dictatess
1996-07-26 paulson 1996-07-26 Redefining "range" as a macro
1996-04-23 oheimb 1996-04-23 *** empty log message ***
1996-04-23 oheimb 1996-04-23 repaired critical proofs depending on the order inside non-confluent SimpSets, (temporarily) removed problematic rule less_Suc_eq form simpset_of "Nat"
1996-03-04 nipkow 1996-03-04 Added a constant UNIV == {x.True} Added many new rewrite rules for sets. Moved LEAST into Nat. Added cardinality to Finite.
1995-11-29 clasohm 1995-11-29 removed quotes from types in consts and syntax sections
1995-10-06 regensbu 1995-10-06 added 8bit pragmas
1995-04-22 nipkow 1995-04-22 HOL.thy: "@" is no longer introduced as a "binder" but has its own explicit translation rule "@x.b" == "Eps(%x.b)". If x is a proper pattern, further translation rules for abstractions with patterns take care of the rest. This is very modular and avoids problems with "binders" such as "!" mentioned below. let now allows pttrn (let (x,y) = t in u) instead of just idt (let x = t in u) Set.thy: UN, INT, ALL, EX, etc all use "pttrn" instead of idt. Same change as for "@" above, except that "@" was a "binder" originally. Prod.thy: Added new syntax for pttrn which allows arbitrarily nested tuples. Two translation rules take care of %pttrn. Unfortunately they cannot be reversed. Hence a little ML-code is used as well. Note that now "! (x,y). ..." is syntactically valid but leads to a translation error. This is because "!" is introduced as a "binder" which means that its translation into lambda-terms is not done by a rewrite rule (aka macro) but by some fixed ML-code which comes after the rewriting stage and does not know how to handle patterns. This looks like a minor blemish since patterns in unbounded quantifiers are not that useful (well, except maybe in unique existence ...). Ideally, there should be two syntactic categories: idts, as we know and love it, which does not admit patterns. patterns, which is what idts has become now. There is one more point where patterns are now allowed but don't make sense: {e | idts . P} where idts is the list of local variables. Univ.thy: converted the defs for <++> and <**> into pattern form. It worked perfectly.
1995-03-03 clasohm 1995-03-03 new version of HOL with curried function application