src/HOL/Product_Type.thy
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-05-31 wenzelm 2005-05-31 tuned;
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2005-02-01 paulson 2005-02-01 the new subst tactic, by Lucas Dixon
2004-12-18 schirmer 2004-12-18 added print translation for split: split f --> %(x,y). f x y
2004-12-13 paulson 2004-12-13 removal of NatArith.ML and Product_Type.ML
2004-12-10 berghofe 2004-12-10 New code generator for let and split.
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-06-16 paulson 2004-06-16 removal of x-symbol syntax <Sigma> for dependent products
2004-04-14 kleing 2004-04-14 use more symbols in HTML output
2004-01-20 schirmer 2004-01-20 Added print translation for pairs
2004-01-05 nipkow 2004-01-05 undid split_comp_eq[simp] because it leads to nontermination together with split_def!
2003-09-26 paulson 2003-09-26 misc tidying
2003-09-15 skalberg 2003-09-15 Fixed blunder in the setup of the classical reasoner wrt. the constant "curry".
2003-09-15 skalberg 2003-09-15 Added the constant "curry".
2003-07-11 oheimb 2003-07-11 added upd_fst, upd_snd, some thms
2002-08-08 wenzelm 2002-08-08 use Tactic.prove instead of prove_goalw_cterm in internal proofs!
2002-08-06 wenzelm 2002-08-06 sane interface for simprocs;
2001-12-01 wenzelm 2001-12-01 renamed class "term" to "type" (actually "HOL.type");
2001-11-09 wenzelm 2001-11-09 eliminated old "symbols" syntax, use "xsymbols" instead;
2001-10-27 wenzelm 2001-10-27 tuned;
2001-10-19 wenzelm 2001-10-19 got rid of ML proof scripts for Product_Type;
2001-10-17 wenzelm 2001-10-17 proper proof of split_paired_all (presently unused);
2001-10-15 wenzelm 2001-10-15 tuned;
2001-09-27 wenzelm 2001-09-27 renamed "()" to Unity, made local;
2001-08-09 oheimb 2001-08-09 added pair_imageI (also as intro rule)
2001-07-25 paulson 2001-07-25 partial restructuring to reduce dependence on Axiom of Choice
2001-07-15 wenzelm 2001-07-15 tuned;
2001-02-02 wenzelm 2001-02-02 added hidden internal_split constant; tuned;
2001-02-01 oheimb 2001-02-01 converted to Isar therory, adding attributes complete_split and split_format
2000-10-23 wenzelm 2000-10-23 tuned deps;
2000-10-12 nipkow 2000-10-12 *** empty log message ***