src/HOL/Set.ML
Tue, 01 Jul 1997 10:37:03 +0200 paulson Now Collect_mem_eq is a default simprule (how could it have ever been omitted?
Fri, 06 Jun 1997 10:20:38 +0200 paulson New miniscoping rules ball_triv and bex_triv
Fri, 16 May 1997 17:40:41 +0200 nipkow Distributed Psubset stuff to basic set theory files, incl Finite.
Fri, 11 Apr 1997 15:21:36 +0200 paulson Yet more fast_tac->blast_tac, and other tidying
Fri, 04 Apr 1997 16:33:28 +0200 nipkow moved inj and surj from Set to Fun and Inv -> inv.
Fri, 04 Apr 1997 11:18:52 +0200 paulson Calls Blast_tac
Thu, 03 Apr 1997 10:29:57 +0200 paulson Declares overloading for set-theoretic constants
Wed, 02 Apr 1997 11:25:04 +0200 paulson Re-ordering of rules to assist blast_tac
Wed, 05 Mar 1997 09:59:55 +0100 paulson New version of InterE, like its ZF counterpart
Wed, 12 Feb 1997 18:53:59 +0100 nipkow New class "order" and accompanying changes.
Thu, 09 Jan 1997 10:23:39 +0100 paulson Tidying of proofs. New theorems are enterred immediately into the
Thu, 26 Sep 1996 12:47:47 +0200 paulson Ran expandshort
Wed, 25 Sep 1996 11:14:18 +0200 paulson Rationalized the rewriting of membership for {} and insert
Thu, 12 Sep 1996 10:40:05 +0200 paulson Tidied many proofs, using AddIffs to let equivalences take
Thu, 22 Aug 1996 12:24:58 +0200 paulson Proved mem_if
Mon, 19 Aug 1996 11:51:39 +0200 paulson Added impOfSubs
Fri, 26 Jul 1996 12:16:17 +0200 paulson Proved bex_False
Fri, 28 Jun 1996 15:28:29 +0200 paulson Added contra_subsetD and rev_contra_subsetD
Tue, 18 Jun 1996 16:38:48 +0200 paulson New rewrites for vacuous quantification
Fri, 31 May 1996 19:12:00 +0200 oheimb moved mem_simps and the corresponding update of !simpset from Fun.ML to Set.ML,
Thu, 23 May 1996 15:16:12 +0200 berghofe equalityI is now added to default claset
Thu, 23 May 1996 14:37:06 +0200 berghofe Replaced fast_tac by Fast_tac (which uses default claset)
Thu, 04 Apr 1996 11:41:35 +0200 paulson Added more _iff rewrites for Compl, Un, Int
Wed, 27 Mar 1996 18:45:17 +0100 paulson Library changes for mutilated checkerboard
Wed, 06 Mar 1996 12:52:11 +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
Fri, 03 Mar 1995 12:02:25 +0100 clasohm new version of HOL with curried function application
less more (0) tip