src/HOL/Set.thy
Mon, 05 Nov 2007 18:18:39 +0100 nipkow added lemmas
Wed, 26 Sep 2007 20:27:58 +0200 haftmann convenient obtain rule for sets
Thu, 20 Sep 2007 16:37:30 +0200 haftmann clarified code lemmas
Fri, 24 Aug 2007 14:14:16 +0200 haftmann made sets executable
Sun, 19 Aug 2007 21:21:37 +0200 nipkow Made UN_Un simp
Fri, 17 Aug 2007 13:58:57 +0200 haftmann dropped junk
Wed, 15 Aug 2007 12:52:56 +0200 paulson ATP blacklisting is now in theory data, attribute noatp
Wed, 15 Aug 2007 08:57:39 +0200 haftmann updated code generator setup
Fri, 20 Jul 2007 14:27:56 +0200 haftmann simplified HOL bootstrap
Thu, 19 Jul 2007 21:47:44 +0200 haftmann code lemma for contents
Sun, 06 May 2007 21:50:17 +0200 haftmann changed code generator invocation syntax
Fri, 20 Apr 2007 11:21:42 +0200 haftmann Isar definitions are now added explicitly to code theorem table
Tue, 20 Mar 2007 08:27:23 +0100 haftmann fixed typo
Fri, 16 Mar 2007 21:32:11 +0100 haftmann added instance of sets as distributive lattices
Mon, 12 Mar 2007 19:23:49 +0100 wenzelm syntax: proper body priorty for derived binders;
Wed, 28 Feb 2007 22:05:43 +0100 wenzelm tuned ML setup;
Wed, 24 Jan 2007 17:10:50 +0100 paulson some new lemmas
Sat, 20 Jan 2007 14:09:27 +0100 wenzelm tuned ML setup;
Wed, 13 Dec 2006 20:38:17 +0100 haftmann dropped FIXME comment
Wed, 13 Dec 2006 15:45:30 +0100 haftmann fixed syntax for bounded quantification
Wed, 06 Dec 2006 01:12:36 +0100 wenzelm removed legacy ML bindings;
Mon, 27 Nov 2006 13:42:42 +0100 haftmann restructured some proofs
Sun, 26 Nov 2006 18:07:16 +0100 wenzelm updated (binder) syntax/notation;
Fri, 17 Nov 2006 02:20:03 +0100 wenzelm more robust syntax for definition/abbreviation/notation;
Wed, 15 Nov 2006 17:05:43 +0100 haftmann moved transitivity rules to Orderings.thy
Mon, 13 Nov 2006 15:43:11 +0100 haftmann dropped LOrder dependency
Sun, 12 Nov 2006 21:31:52 +0100 nipkow image_constant_conv no longer [simp]
Sun, 12 Nov 2006 19:22:10 +0100 nipkow started reorgnization of lattice theories
Tue, 07 Nov 2006 11:47:57 +0100 wenzelm renamed 'const_syntax' to 'notation';
Mon, 14 Aug 2006 13:46:06 +0200 haftmann simplified code generator setup
Wed, 26 Jul 2006 19:23:04 +0200 webertj linear arithmetic splits certain operators (e.g. min, max, abs)
Tue, 13 Jun 2006 15:07:58 +0200 paulson new results
Tue, 16 May 2006 21:33:01 +0200 wenzelm tuned concrete syntax -- abbreviation/const_syntax;
Sat, 13 May 2006 21:13:25 +0200 wenzelm reactivated translations for less/less_eq;
Sat, 08 Apr 2006 22:51:06 +0200 wenzelm refined 'abbreviation';
Thu, 23 Mar 2006 20:03:53 +0100 nipkow Converted translations to abbbreviations.
Mon, 20 Mar 2006 17:38:22 +0100 paulson subsetI is often necessary
Fri, 17 Mar 2006 09:34:23 +0100 haftmann renamed op < <= to Orderings.less(_eq)
Fri, 10 Mar 2006 15:33:48 +0100 haftmann renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
Thu, 02 Mar 2006 18:50:43 +0100 paulson subset_refl now included using the atp attribute
Mon, 30 Jan 2006 08:20:56 +0100 haftmann adaptions to codegen_package
Sun, 29 Jan 2006 19:23:38 +0100 wenzelm declare 'defn' rules;
Fri, 13 Jan 2006 14:43:09 +0100 nipkow *** empty log message ***
Wed, 21 Dec 2005 12:02:57 +0100 paulson removed or modified some instances of [iff]
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
less more (0) -100 -60 tip