src/HOL/Set.thy
Thu, 04 Mar 2010 15:44:06 +0100 hoelzl Added vimage_inter_cong
Mon, 01 Mar 2010 13:40:23 +0100 haftmann replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
Thu, 11 Feb 2010 23:00:22 +0100 wenzelm modernized translations;
Thu, 04 Feb 2010 14:45:08 +0100 hoelzl Changed 'bounded unique existential quantifiers' from a constant to syntax translation.
Thu, 28 Jan 2010 11:48:49 +0100 haftmann new theory Algebras.thy for generic algebraic structures
Wed, 30 Dec 2009 10:24:53 +0100 krauss killed a few warnings
Fri, 27 Nov 2009 16:26:23 +0100 berghofe Removed eq_to_mono2, added not_mono.
Mon, 09 Nov 2009 15:50:15 +0000 paulson New theory Probability/Borel.thy, and some associated lemmas
Wed, 21 Oct 2009 11:19:11 +0100 paulson merged
Tue, 20 Oct 2009 16:32:51 +0100 paulson Some new lemmas concerning sets
Wed, 21 Oct 2009 08:16:25 +0200 haftmann merged
Wed, 21 Oct 2009 08:14:38 +0200 haftmann dropped redundant gen_ prefix
Tue, 20 Oct 2009 16:13:01 +0200 haftmann replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
Tue, 20 Oct 2009 15:02:48 +0100 paulson Removal of the unused atpset concept, the atp attribute and some related code.
Wed, 07 Oct 2009 14:01:26 +0200 haftmann tuned proofs
Sat, 19 Sep 2009 07:38:03 +0200 haftmann inter and union are mere abbreviations for inf and sup
Mon, 31 Aug 2009 14:09:42 +0200 nipkow tuned the simp rules for Int involving insert and intervals.
Tue, 28 Jul 2009 13:37:09 +0200 haftmann Set.UNIV and Set.empty are mere abbreviations for top and bot
Wed, 22 Jul 2009 18:02:10 +0200 haftmann moved complete_lattice &c. into separate theory
Wed, 22 Jul 2009 14:20:32 +0200 haftmann set intersection and union now named inter and union; closer connection between set and lattice operations; factored out complete lattice
Tue, 21 Jul 2009 14:38:07 +0200 haftmann attempt for more concise setup of non-etacontracting binders
Tue, 21 Jul 2009 11:09:50 +0200 haftmann Set.thy: prefer = over == where possible; tuned ML setup; dropped (moved) ML legacy
Tue, 21 Jul 2009 07:54:44 +0200 haftmann swapped bootstrap order of UNION/Union and INTER/Inter in theory Set
Mon, 20 Jul 2009 15:24:15 +0200 haftmann less digestible
Mon, 20 Jul 2009 11:47:17 +0200 haftmann refined outline structure
Mon, 20 Jul 2009 09:52:09 +0200 haftmann merged
Mon, 20 Jul 2009 08:31:12 +0200 haftmann closer relation of sets and complete lattices; corresponding consts, defs and syntax at similar places in theory text
Mon, 20 Jul 2009 08:32:07 +0200 haftmann merged
Tue, 14 Jul 2009 15:54:19 +0200 haftmann refinement of lattice classes
Wed, 15 Jul 2009 23:48:21 +0200 wenzelm more antiquotations;
Sat, 11 Jul 2009 21:33:01 +0200 haftmann added boolean_algebra type class; tuned lattice duals
Mon, 06 Jul 2009 21:24:30 +0200 wenzelm structure Thm: less pervasive names;
Mon, 15 Jun 2009 16:13:19 +0200 haftmann authentic syntax for Pow and image
Fri, 05 Jun 2009 08:06:03 +0200 haftmann merged
Thu, 04 Jun 2009 15:28:59 +0200 haftmann insert now qualified and with authentic syntax
Thu, 04 Jun 2009 19:44:06 +0200 nipkow finite lemmas
Mon, 18 May 2009 23:15:38 +0200 nipkow fine-tuned elimination of comprehensions involving x=t.
Sat, 16 May 2009 11:28:02 +0200 nipkow "{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
Tue, 31 Mar 2009 13:23:39 +0200 wenzelm tuned;
Thu, 19 Mar 2009 14:08:41 +0100 haftmann tuned some theorem and attribute bindings
Sat, 14 Mar 2009 12:50:29 +0100 haftmann reverted to old version of Set.thy -- strange effects have to be traced first
Sat, 07 Mar 2009 15:20:32 +0100 haftmann restructured theory Set.thy
Thu, 05 Mar 2009 08:23:11 +0100 haftmann set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
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
less more (0) -100 -60 tip