src/HOL/Finite.ML
1998-04-27 nipkow 1998-04-27 Added a few lemmas. Renamed expand_const -> split_const.
1998-04-03 paulson 1998-04-03 Tidied proofs
1998-04-02 paulson 1998-04-02 New theorems card_Diff_le and card_insert_le; tidied
1998-03-30 oheimb 1998-03-30 adapted proof of finite_converse
1998-03-16 paulson 1998-03-16 inverse -> converse [It is standard terminology and also used in ZF]
1998-03-07 nipkow 1998-03-07 Removed `addsplits [expand_if]'
1997-12-24 paulson 1997-12-24 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
1997-12-16 wenzelm 1997-12-16 expandshort;
1997-12-11 paulson 1997-12-11 Tidied proof of finite_subset_induct
1997-11-26 paulson 1997-11-26 Tidying
1997-11-05 paulson 1997-11-05 Ran expandshort, especially to introduce Safe_tac
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-11-01 paulson 1997-11-01 New Blast_tac (and minor tidying...)
1997-10-28 nipkow 1997-10-28 Added finite_UNION/SigmaI.
1997-10-17 nipkow 1997-10-17 setloop split_tac -> addsplits
1997-10-17 paulson 1997-10-17 Better simplification eliminates a command from proof of psubset_card
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-09-29 paulson 1997-09-29 Step_tac -> Safe_tac
1997-09-25 paulson 1997-09-25 Changed some proofs to use Clarify_tac
1997-07-14 paulson 1997-07-14 Removed redundant addsimps of Un_insert_left, which is now a default simprule
1997-06-23 paulson 1997-06-23 Ran expandshort
1997-06-17 nipkow 1997-06-17 converse -> ^-1
1997-06-06 wenzelm 1997-06-06 eliminated non-ASCII;
1997-06-06 paulson 1997-06-06 Removed a few redundant additions of simprules or classical rules
1997-06-05 nipkow 1997-06-05 added finite_converse
1997-06-05 nipkow 1997-06-05 Moved image_is_empty from Finite.ML to equalities.ML
1997-06-05 nipkow 1997-06-05 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'. Relation.ML Trancl.ML: more thms WF.ML WF.thy: added `acyclic' WF_Rel.ML: moved some thms back into WF and added some new ones.
1997-06-03 paulson 1997-06-03 New theorem about the cardinality of the powerset (uses exponentiation)
1997-06-02 paulson 1997-06-02 Simplified proof
1997-05-30 paulson 1997-05-30 Many new theorems about cardinality
1997-05-27 paulson 1997-05-27 New theorems suggested by Florian Kammueller
1997-05-26 paulson 1997-05-26 Two results suggested by Florian Kammueller
1997-05-16 nipkow 1997-05-16 Distributed Psubset stuff to basic set theory files, incl Finite. Added stuff by bu.
1997-04-09 paulson 1997-04-09 Using Blast_tac
1996-09-26 paulson 1996-09-26 Ran expandshort
1996-06-03 berghofe 1996-06-03 best_tac, deepen_tac and safe_tac now also use default claset.
1996-06-03 paulson 1996-06-03 Shortened a proof
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-04-17 oheimb 1996-04-17 *** empty log message ***
1996-03-27 paulson 1996-03-27 Library changes for mutilated checkerboard
1996-03-06 paulson 1996-03-06 Ran expandshort
1996-03-06 nipkow 1996-03-06 Added 'section' commands
1996-03-04 nipkow 1996-03-04 Added a constant UNIV == {x.True} Added many new rewrite rules for sets. Moved LEAST into Nat. Added cardinality to Finite.
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-03-03 clasohm 1995-03-03 new version of HOL with curried function application