src/HOL/Finite.ML
Mon, 22 Jun 1998 17:26:46 +0200 wenzelm isatool fixgoal;
Mon, 27 Apr 1998 16:45:11 +0200 nipkow Added a few lemmas.
Fri, 03 Apr 1998 11:22:51 +0200 paulson Tidied proofs
Thu, 02 Apr 1998 13:47:03 +0200 paulson New theorems card_Diff_le and card_insert_le; tidied
Mon, 30 Mar 1998 21:09:46 +0200 oheimb adapted proof of finite_converse
Mon, 16 Mar 1998 16:50:50 +0100 paulson inverse -> converse
Sat, 07 Mar 1998 16:29:29 +0100 nipkow Removed `addsplits [expand_if]'
Wed, 24 Dec 1997 10:02:30 +0100 paulson New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
Tue, 16 Dec 1997 17:58:03 +0100 wenzelm expandshort;
Thu, 11 Dec 1997 10:29:22 +0100 paulson Tidied proof of finite_subset_induct
Wed, 26 Nov 1997 17:27:34 +0100 paulson Tidying
Wed, 05 Nov 1997 13:23:46 +0100 paulson Ran expandshort, especially to introduce Safe_tac
Mon, 03 Nov 1997 12:13:18 +0100 wenzelm isatool fixclasimp;
Sat, 01 Nov 1997 12:59:06 +0100 paulson New Blast_tac (and minor tidying...)
Tue, 28 Oct 1997 14:03:25 +0100 nipkow Added finite_UNION/SigmaI.
Fri, 17 Oct 1997 15:25:12 +0200 nipkow setloop split_tac -> addsplits
Fri, 17 Oct 1997 10:58:44 +0200 paulson Better simplification eliminates a command from proof of psubset_card
Fri, 10 Oct 1997 19:02:28 +0200 wenzelm fixed dots;
Mon, 29 Sep 1997 11:37:02 +0200 paulson Step_tac -> Safe_tac
Thu, 25 Sep 1997 12:13:18 +0200 paulson Changed some proofs to use Clarify_tac
Mon, 14 Jul 1997 12:42:28 +0200 paulson Removed redundant addsimps of Un_insert_left, which is now a default simprule
Mon, 23 Jun 1997 10:42:03 +0200 paulson Ran expandshort
Tue, 17 Jun 1997 09:01:56 +0200 nipkow converse -> ^-1
Fri, 06 Jun 1997 21:49:47 +0200 wenzelm eliminated non-ASCII;
Fri, 06 Jun 1997 13:28:40 +0200 paulson Removed a few redundant additions of simprules or classical rules
Thu, 05 Jun 1997 19:44:13 +0200 nipkow added finite_converse
Thu, 05 Jun 1997 17:19:05 +0200 nipkow Moved image_is_empty from Finite.ML to equalities.ML
Thu, 05 Jun 1997 14:39:22 +0200 nipkow Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
Tue, 03 Jun 1997 10:53:58 +0200 paulson New theorem about the cardinality of the powerset (uses exponentiation)
Mon, 02 Jun 1997 12:12:57 +0200 paulson Simplified proof
Fri, 30 May 1997 15:17:14 +0200 paulson Many new theorems about cardinality
Tue, 27 May 1997 13:03:41 +0200 paulson New theorems suggested by Florian Kammueller
Mon, 26 May 1997 12:36:56 +0200 paulson Two results suggested by Florian Kammueller
Fri, 16 May 1997 17:40:41 +0200 nipkow Distributed Psubset stuff to basic set theory files, incl Finite.
Wed, 09 Apr 1997 12:32:04 +0200 paulson Using Blast_tac
Thu, 26 Sep 1996 12:47:47 +0200 paulson Ran expandshort
Mon, 03 Jun 1996 17:10:56 +0200 berghofe best_tac, deepen_tac and safe_tac now also use default claset.
Mon, 03 Jun 1996 11:41:00 +0200 paulson Shortened a proof
Thu, 23 May 1996 14:37:06 +0200 berghofe Replaced fast_tac by Fast_tac (which uses default claset)
Wed, 17 Apr 1996 17:59:58 +0200 oheimb *** empty log message ***
Wed, 27 Mar 1996 18:45:17 +0100 paulson Library changes for mutilated checkerboard
Wed, 06 Mar 1996 13:57:07 +0100 paulson Ran expandshort
Wed, 06 Mar 1996 10:05:00 +0100 nipkow Added 'section' commands
Mon, 04 Mar 1996 14:37:33 +0100 nipkow Added a constant UNIV == {x.True}
Tue, 30 Jan 1996 15:24:36 +0100 clasohm expanded tabs
Wed, 04 Oct 1995 13:10:03 +0100 clasohm added local simpsets; removed IOA from 'make test'
Fri, 03 Mar 1995 12:02:25 +0100 clasohm new version of HOL with curried function application
less more (0) tip