src/HOL/Set.thy
Fri, 16 Dec 2005 16:59:32 +0100 nipkow new lemmas
Thu, 15 Dec 2005 19:42:00 +0100 wenzelm removed obsolete/unused setup_induction;
Thu, 01 Dec 2005 22:04:27 +0100 wenzelm simprocs: static evaluation of simpset;
Thu, 01 Dec 2005 15:45:54 +0100 paulson restoring the old status of subset_refl
Thu, 10 Nov 2005 17:33:14 +0100 paulson duplicate axioms in ATP linkup, and general fixes
Mon, 17 Oct 2005 23:10:10 +0200 wenzelm change_claset/simpset;
Fri, 07 Oct 2005 22:59:22 +0200 wenzelm Term.absdummy;
Thu, 29 Sep 2005 12:43:40 +0200 paulson a name for empty_not_insert
Thu, 29 Sep 2005 00:58:55 +0200 wenzelm more finalconsts;
Thu, 22 Sep 2005 23:56:15 +0200 nipkow renamed rules to iprover
Tue, 20 Sep 2005 14:03:37 +0200 wenzelm tuned theory dependencies;
Tue, 16 Aug 2005 18:53:11 +0200 paulson more simprules now have names
Tue, 16 Aug 2005 15:36:28 +0200 paulson classical rules must have names for ATP integration
Tue, 02 Aug 2005 19:47:12 +0200 wenzelm simprocs: Simplifier.inherit_bounds;
Tue, 12 Jul 2005 12:49:00 +0200 paulson tweaked
Fri, 01 Jul 2005 13:57:53 +0200 berghofe Added strong_ball_cong and strong_bex_cong (these are now the standard
Wed, 11 May 2005 09:50:33 +0200 nipkow Added thms by Brian Huffmann
Tue, 01 Mar 2005 18:48:52 +0100 nipkow integrated Jeremy's FiniteLib
Fri, 18 Feb 2005 11:48:42 +0100 nipkow tuning
Thu, 10 Feb 2005 18:51:12 +0100 nipkow Moved oderings from HOL into the new Orderings.thy
Mon, 27 Sep 2004 10:27:34 +0200 ballarin Modified locales: improved implementation of "includes".
Wed, 18 Aug 2004 11:09:40 +0200 nipkow import -> imports
Mon, 16 Aug 2004 14:22:27 +0200 nipkow New theory header syntax.
Fri, 06 Aug 2004 16:55:14 +0200 nipkow undid UN/INT syntax
Tue, 03 Aug 2004 13:48:00 +0200 paulson new simprules Int_subset_iff and Un_subset_iff
Mon, 21 Jun 2004 10:25:57 +0200 kleing Merged in license change from Isabelle2004
Sat, 29 May 2004 15:11:43 +0200 wenzelm \<^bsub>/\<^esub> syntax: unbreakable block;
Fri, 28 May 2004 11:19:15 +0200 paulson new theorem Collect_imp_eq
Wed, 26 May 2004 14:57:06 +0200 nipkow Corrected printer bug for bounded quantifiers Q x<=y. P
Mon, 17 May 2004 11:02:16 +0200 mehta lemma disjoint_int_union removed - too special
Thu, 13 May 2004 16:02:29 +0200 mehta New simp rules added:
Sat, 01 May 2004 22:04:14 +0200 wenzelm improved subscript syntax;
Wed, 14 Apr 2004 14:13:05 +0200 kleing use more symbols in HTML output
Tue, 13 Apr 2004 09:42:40 +0200 ballarin Various changes to HOL-Algebra;
Wed, 24 Mar 2004 10:50:29 +0100 paulson streamlined treatment of quotients for the integers
Thu, 19 Feb 2004 15:57:34 +0100 ballarin Efficient, graph-based reasoner for linear and partial orders.
Wed, 11 Feb 2004 01:26:15 +0100 nipkow Modified UN and INT xsymbol syntax: made index subscript
Thu, 01 Jan 2004 21:47:07 +0100 paulson conversion of Real/PReal to Isar script;
Fri, 19 Dec 2003 04:28:45 +0100 nipkow *** empty log message ***
Fri, 26 Sep 2003 10:34:57 +0200 paulson misc tidying
Fri, 11 Jul 2003 14:11:56 +0200 oheimb added rev_ballE
Mon, 17 Mar 2003 17:37:20 +0100 paulson moved one proof, added another
Fri, 14 Mar 2003 10:30:15 +0100 paulson new UN/INT simprules
Tue, 11 Mar 2003 15:19:27 +0100 nipkow *** empty log message ***
Wed, 26 Feb 2003 10:44:54 +0100 paulson new lemma
Tue, 25 Feb 2003 12:42:08 +0100 nipkow Undid eta change for UN/INT.
Sun, 16 Feb 2003 12:16:07 +0100 paulson new theorem Compl_partition2
Sun, 22 Dec 2002 15:02:40 +0100 nipkow removed some problems with print translations
Sun, 22 Dec 2002 10:43:43 +0100 nipkow added print translations tha avoid eta contraction for important binders.
Fri, 18 Oct 2002 09:53:02 +0200 nipkow Added a few thms about UN/INT/{}/UNIV
Thu, 03 Oct 2002 10:34:51 +0200 paulson added the new elim rule psubsetE
Fri, 30 Aug 2002 16:42:45 +0200 paulson removal of blast.overloaded
Tue, 06 Aug 2002 11:22:05 +0200 wenzelm sane interface for simprocs;
Wed, 24 Jul 2002 22:15:55 +0200 wenzelm simplified locale predicates;
Tue, 07 May 2002 19:54:04 +0200 wenzelm rev_bexI [intro?];
Mon, 06 May 2002 09:42:20 +0200 nipkow Added insert_disjoint and disjoint_insert [simp], and simplified proofs
Mon, 25 Feb 2002 20:48:14 +0100 wenzelm clarified syntax of ``long'' statements: fixes/assumes/shows;
Sat, 16 Feb 2002 20:59:34 +0100 wenzelm converted/deleted equalities.ML, mono.ML, subset.ML (see Set.thy);
Fri, 04 Jan 2002 19:29:30 +0100 wenzelm tuned ``syntax (output)'';
Sat, 01 Dec 2001 18:52:32 +0100 wenzelm renamed class "term" to "type" (actually "HOL.type");
less more (0) -100 -60 tip