src/HOL/Product_Type.thy
2006-02-10 haftmann 2006-02-10 improved code generator devarification
2006-02-07 haftmann 2006-02-07 slight improvements in code generation
2006-01-23 haftmann 2006-01-23 removed problematic keyword 'atom'
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2006-01-19 berghofe 2006-01-19 Re-inserted consts_code declaration accidentally deleted during last commit.
2006-01-17 haftmann 2006-01-17 substantial improvements in code generator
2005-12-29 haftmann 2005-12-29 adaptions to changes in code generator
2005-12-08 wenzelm 2005-12-08 tuned proofs;
2005-12-02 haftmann 2005-12-02 adjusted to improved code generator interface
2005-12-01 wenzelm 2005-12-01 simprocs: static evaluation of simpset;
2005-11-22 haftmann 2005-11-22 added codegenerator
2005-10-28 haftmann 2005-10-28 added extraction interface for code generator
2005-10-21 wenzelm 2005-10-21 Goal.prove;
2005-10-17 wenzelm 2005-10-17 change_claset/simpset; Simplifier.inherit_context instead of Simplifier.inherit_bounds;
2005-10-07 wenzelm 2005-10-07 replaced _K by dummy abstraction;
2005-08-16 paulson 2005-08-16 more simprules now have names
2005-08-03 berghofe 2005-08-03 Fixed bug in code generator for let and split leading to ill-formed code.
2005-08-02 wenzelm 2005-08-02 simprocs: Simplifier.inherit_bounds;
2005-07-12 berghofe 2005-07-12 Auxiliary functions to be used in generated code are now defined using "attach".
2005-07-01 berghofe 2005-07-01 Adapted to new interface of code generator.
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 ***