src/HOL/Sum.ML
1999-08-19 berghofe 1999-08-19 Moved sum_case stuff from Sum to Datatype.
1999-08-18 berghofe 1999-08-18 Renamed sum_case to basic_sum_case and removed translations for sum_case to avoid conflicts with the constant sum_case introduced in Datatype.thy.
1999-07-27 paulson 1999-07-27 tidied
1999-07-19 paulson 1999-07-19 getting rid of qed_goal
1999-07-16 berghofe 1999-07-16 Added some definitions and theorems needed for the construction of datatypes involving function types.
1998-08-13 paulson 1998-08-13 even more tidying of Goal commands
1998-07-24 berghofe 1998-07-24 Adapted to new datatype package.
1998-07-15 paulson 1998-07-15 More tidying and removal of "\!\!... from Goal commands
1998-07-15 paulson 1998-07-15 Removal of leading "\!\!..." from most Goal commands
1998-06-22 wenzelm 1998-06-22 isatool fixgoal;
1998-06-02 oheimb 1998-06-02 added split_sum_case_asm
1998-04-27 nipkow 1998-04-27 Added a few lemmas. Renamed expand_const -> split_const.
1998-01-08 oheimb 1998-01-08 added select_equality to the implicit claset
1997-12-24 paulson 1997-12-24 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-05-02 paulson 1997-05-02 New blast_tac call: made possible by bug fix involving equality substitution
1997-04-09 paulson 1997-04-09 Using Blast_tac
1997-04-04 paulson 1997-04-04 Calls Blast_tac
1996-11-20 nipkow 1996-11-20 plus -> Plus to avoid hiding class plus
1996-09-12 paulson 1996-09-12 Tidied many proofs, using AddIffs to let equivalences take the place of separate Intr and Elim rules. Also deleted most named clasets.
1996-05-23 berghofe 1996-05-23 Removed equalityI from some proofs (because it is now included in the default claset)
1996-05-23 berghofe 1996-05-23 Replaced fast_tac by Fast_tac (which uses default claset) New rules are now also added to default claset.
1996-02-19 nipkow 1996-02-19 Introduced normalize_thm into HOL.ML Corrected some dependencies among Sum, Prod and mono. Extended RelPow
1996-01-30 clasohm 1996-01-30 expanded tabs
1995-10-04 clasohm 1995-10-04 added local simpsets; removed IOA from 'make test'
1995-07-25 lcp 1995-07-25 Added Part_Int and Part_Collect for inductive definitions
1995-03-03 clasohm 1995-03-03 new version of HOL with curried function application