src/HOL/Prod.thy
1997-04-03 nipkow 1997-04-03 Now: unit = {True}
1997-04-03 nipkow 1997-04-03 Removed (Unit) in Prod. Added test for ancestor Nat in datatype.
1996-12-13 oheimb 1996-12-13 adaptions for symbol font
1996-11-27 wenzelm 1996-11-27 added symbols syntax;
1996-05-24 nipkow 1996-05-24 Removed junk introduced by a cvs merge.
1996-05-21 berghofe 1996-05-21 Added additional parent theory equalities because some proofs in Prod.ML depend on rules proved in equalities.ML
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-04-17 oheimb 1996-04-17 *** empty log message ***
1996-04-11 nipkow 1996-04-11 Added a number of lemmas
1996-04-03 nipkow 1996-04-03 Introduced Times and SIGMA.
1996-03-08 clasohm 1996-03-08 added constdefs section
1996-02-05 clasohm 1996-02-05 expanded tabs; renamed subtype to typedef; incorporated Konrad's changes
1996-01-26 nipkow 1996-01-26 Streamlined defs in Relation and added new intro/elim rules to do with pattern matching in sets: {(x,y). ...} and UN (x,y):A. ...
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-05-09 nipkow 1995-05-09 Prod is now a parent of Lfp. Added thm induct2 to Lfp. Changed the way patterns in abstractions are pretty printed. It has become simpler now but fails if split has more than one argument because then the ast-translation does not match.
1995-05-03 nipkow 1995-05-03 Corrected display of split f t: no more let. Also replaced "_abs" by "_lambda" --- the former was a mistake which happended to work.
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-24 clasohm 1995-03-24 changed syntax of tuples from <..., ...> to (..., ...)
1995-03-21 clasohm 1995-03-21 changed syntax of Unity ("()" instead of "<>")
1995-03-03 clasohm 1995-03-03 new version of HOL with curried function application