src/HOL/Set.thy
Fri, 13 Feb 2009 23:55:04 +0100 nipkow finiteness lemmas
Thu, 29 Jan 2009 22:28:03 +0100 berghofe Added strong congruence rule for UN.
Fri, 10 Oct 2008 06:45:53 +0200 haftmann `code func` now just `code`
Mon, 11 Aug 2008 14:50:00 +0200 haftmann rudimentary code setup for set operations
Tue, 01 Jul 2008 06:51:59 +0200 huffman remove simp attribute from range_composition
Tue, 10 Jun 2008 15:30:56 +0200 haftmann removed some dubious code lemmas
Wed, 07 May 2008 10:56:43 +0200 berghofe - Now uses Orderings as parent theory
Tue, 22 Apr 2008 08:33:16 +0200 haftmann constant HOL.eq now qualified
Wed, 02 Apr 2008 15:58:32 +0200 haftmann explicit class "eq" for operational equality
Sat, 29 Mar 2008 19:14:00 +0100 wenzelm replaced 'ML_setup' by 'ML';
Wed, 19 Mar 2008 22:47:35 +0100 wenzelm eliminated change_claset/simpset;
Tue, 26 Feb 2008 20:38:15 +0100 haftmann moved some set lemmas from Set.thy here
Fri, 25 Jan 2008 14:54:41 +0100 haftmann improved code theorem setup
Wed, 02 Jan 2008 15:14:02 +0100 haftmann splitted class uminus from class minus
Fri, 30 Nov 2007 20:13:03 +0100 haftmann adjustions to due to instance target
Thu, 29 Nov 2007 17:08:26 +0100 haftmann instance command as rudimentary class target
Fri, 23 Nov 2007 21:09:33 +0100 haftmann interpretation of typedecls: instantiation to class type
Fri, 09 Nov 2007 13:41:27 +0100 krauss avoid name clashes when generating code for union, inter
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;
less more (0) -100 -60 tip