src/HOL/Prod.ML
1998-04-27 nipkow 1998-04-27 Added a few lemmas. Renamed expand_const -> split_const.
1998-04-24 oheimb 1998-04-24 improved split_all_tac significantly
1998-04-21 oheimb 1998-04-21 improved pair_tac to call prune_params_tac afterwards improved the (bad) efficiency of split_all_tac by about 50% split_all_tac is now added to claset() _before_ other safe tactics
1998-04-07 oheimb 1998-04-07 made split_all_tac as safe wrapper more defensive: if it is added as unsafe wrapper again (as its was before), this does not break the current proofs.
1998-04-02 oheimb 1998-04-02 split_all_tac now fails if there is nothing to split split_all_tac has moved within claset() from usafe wrappers to safe wrappers
1998-02-25 oheimb 1998-02-25 added split_all_tac to claset()
1998-01-08 oheimb 1998-01-08 added select_equality to the implicit claset added split_paired_Ex, split_part, and Eps_split_eq to the implicit simpset removed split_select renamed Collect_Prod to Collect_split
1998-01-08 paulson 1998-01-08 Tidied by adding more default simprules
1997-12-18 oheimb 1997-12-18 added expand_split_asm
1997-12-16 wenzelm 1997-12-16 expandshort;
1997-11-10 oheimb 1997-11-10 replaced 8bit characters
1997-11-04 oheimb 1997-11-04 added several theorems
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-10-17 nipkow 1997-10-17 setloop split_tac -> addsplits
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-07-23 nipkow 1997-07-23 Prod.ML: Added split_paired_EX and lots of comments about failed attempts to automate reasoning about products. simpdata.ML: added simplification procedure for simplifying existential statements of the form ? x. ... & x = t & ...
1997-06-06 nipkow 1997-06-06 Added AddIffs [Pair_eq]; which made AddSEs [Pair_inject]; redundant.
1997-04-11 paulson 1997-04-11 Yet more fast_tac->blast_tac, and other tidying
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.
1997-04-02 paulson 1997-04-02 Reorganization of how classical rules are installed
1997-02-15 oheimb 1997-02-15 reflecting my recent changes of the simplifier and classical reasoner
1996-10-10 paulson 1996-10-10 Deleted obsolete clasets
1996-09-26 paulson 1996-09-26 Ran expandshort
1996-05-21 berghofe 1996-05-21 Replaced fast_tac by Fast_tac (which uses default claset) New rules are now also added to default claset.
1996-05-17 nipkow 1996-05-17 Moved split_rule et al from ind_syntax.ML to Prod.ML. Used split_rule in Lfp.ML and Trancl.ML.
1996-05-07 paulson 1996-05-07 Now split_all_tac works for i>1 !
1996-04-11 nipkow 1996-04-11 Added a number of lemmas
1996-04-04 paulson 1996-04-04 Using new "Times" infix
1996-03-27 paulson 1996-03-27 Library changes for mutilated checkerboard
1996-03-06 paulson 1996-03-06 Ran expandshort
1996-02-19 nipkow 1996-02-19 Introduced normalize_thm into HOL.ML Corrected some dependencies among Sum, Prod and mono. Extended RelPow
1996-02-09 nipkow 1996-02-09 Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
1996-01-30 clasohm 1996-01-30 expanded tabs
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-10-25 nipkow 1995-10-25 Added various thms and tactics.
1995-10-04 clasohm 1995-10-04 added local simpsets; removed IOA from 'make test'
1995-03-24 clasohm 1995-03-24 changed syntax of tuples from <..., ...> to (..., ...)
1995-03-03 clasohm 1995-03-03 new version of HOL with curried function application