src/HOL/Library/Multiset.thy
Sun, 02 Jun 2013 20:44:55 +0200 haftmann type class for confined subtraction
Thu, 04 Apr 2013 22:46:14 +0200 haftmann sup on multisets
Wed, 03 Apr 2013 22:26:04 +0200 haftmann default implementation of multisets by list with reasonable coverage of operations on multisets
Wed, 03 Apr 2013 22:26:04 +0200 haftmann optionalized very specific code setup for multisets
Wed, 27 Mar 2013 10:55:05 +0100 haftmann centralized various multiset operations in theory multiset;
Fri, 15 Feb 2013 11:47:34 +0100 haftmann attempt to re-establish conventions which theories are loaded into the grand unified library theory;
Fri, 15 Feb 2013 08:31:31 +0100 haftmann two target language numeral types: integer and natural, as replacement for code_numeral;
Thu, 14 Feb 2013 15:27:10 +0100 haftmann reform of predicate compiler / quickcheck theories:
Fri, 12 Oct 2012 18:58:20 +0200 wenzelm discontinued obsolete typedef (open) syntax;
Thu, 11 Oct 2012 11:56:43 +0200 haftmann avoid global interpretation
Thu, 11 Oct 2012 11:56:42 +0200 haftmann simplified construction of fold combinator on multisets;
Thu, 04 Oct 2012 23:19:02 +0200 haftmann default simp rule for image under identity
Sun, 16 Sep 2012 06:51:36 +0200 bulwahn removing find_theorems commands that were left in the developments accidently
Sat, 15 Sep 2012 20:14:29 +0200 haftmann typeclass formalising bounded subtraction
Tue, 29 May 2012 17:53:43 +0200 huffman add lemma set_of_image_mset
Tue, 29 May 2012 17:06:04 +0200 huffman reordered sections
Tue, 29 May 2012 11:41:37 +0200 huffman shortened yet more multiset proofs;
Tue, 29 May 2012 11:30:13 +0200 huffman remove unused intermediate lemma
Tue, 29 May 2012 11:13:00 +0200 huffman shortened more multiset proofs
Tue, 29 May 2012 10:30:47 +0200 huffman shortened some proofs
Tue, 29 May 2012 10:08:31 +0200 huffman use transfer method for instance proof
Thu, 12 Apr 2012 10:13:33 +0200 bulwahn multiset operations are defined with lift_definitions;
Tue, 03 Apr 2012 16:26:48 +0200 kuncar new package Lifting - initial commit
Thu, 29 Mar 2012 21:13:48 +0200 kuncar use qualified names for rsp and rep_eq theorems in quotient_def
Wed, 28 Mar 2012 10:16:02 +0200 bulwahn changing more definitions to quotient_definition
Wed, 28 Mar 2012 10:00:52 +0200 bulwahn using abstract code equations for proofs of code equations in Multiset
Tue, 27 Mar 2012 14:14:46 +0200 bulwahn association lists with distinct keys uses the quotient infrastructure to obtain code certificates;
Wed, 14 Mar 2012 15:59:39 +0100 wenzelm some proof indentation;
Fri, 02 Mar 2012 09:35:32 +0100 bulwahn adding finiteness of intervals on integer sets; adding another finiteness theorem for multisets
Tue, 28 Feb 2012 20:20:09 +0100 wenzelm tuned proofs;
Wed, 01 Feb 2012 15:28:02 +0100 bulwahn improving code equations for multisets that violated the distinct AList abstraction
Tue, 17 Jan 2012 10:45:42 +0100 bulwahn renaming theory AList_Impl back to AList (reverting 1fec5b365f9b; AList with distinct key invariant is called DAList)
Tue, 17 Jan 2012 09:38:30 +0100 bulwahn renamed theory AList to DAList
Tue, 10 Jan 2012 10:17:09 +0100 bulwahn improving code generation for multisets; adding exhaustive quickcheck generators for multisets
Mon, 26 Dec 2011 22:17:10 +0100 haftmann moved theorem requiring multisets from More_List to Multiset
Wed, 14 Dec 2011 15:56:29 +0100 bulwahn adding code attribute to enable evaluation of equality on multisets
Wed, 30 Nov 2011 16:27:10 +0100 wenzelm prefer typedef without extra definition and alternative name;
Sun, 20 Nov 2011 21:28:07 +0100 wenzelm eliminated obsolete "standard";
Mon, 12 Sep 2011 07:55:43 +0200 nipkow new fastforce replacing fastsimp - less confusing name
Sat, 20 Aug 2011 23:36:18 +0200 wenzelm odd workaround for odd problem of load order in HOL/ex/ROOT.ML (!??);
Fri, 20 May 2011 11:44:16 +0200 haftmann names of fold_set locales resemble name of characteristic property more closely
Sat, 14 May 2011 18:26:25 +0200 haftmann use pointfree characterisation for fold_set locale
Tue, 11 Jan 2011 14:12:37 +0100 haftmann "enriched_type" replaces less specific "type_lifting"
Tue, 21 Dec 2010 17:52:23 +0100 haftmann tuned type_lifting declarations
Tue, 07 Dec 2010 16:33:54 +0100 haftmann name filter operation just filter (c.f. List.filter and list comprehension syntax)
Mon, 06 Dec 2010 09:19:10 +0100 haftmann replace `type_mapper` by the more adequate `type_lifting`
Fri, 03 Dec 2010 22:34:20 +0100 haftmann lemma multiset_of_rev
Thu, 18 Nov 2010 17:01:16 +0100 haftmann mapper for mulitset type
Wed, 03 Nov 2010 12:15:47 +0100 haftmann added code lemmas for stable parametrized quicksort
Wed, 03 Nov 2010 11:50:29 +0100 haftmann tuned proof
Tue, 02 Nov 2010 16:59:40 +0100 haftmann tuned proof
Tue, 02 Nov 2010 16:48:19 +0100 haftmann tuned proof
Tue, 02 Nov 2010 16:36:33 +0100 haftmann tuned lemma proposition of properties_for_sort_key
Tue, 02 Nov 2010 16:31:56 +0100 haftmann lemmas multiset_of_filter, sort_key_by_quicksort
Fri, 29 Oct 2010 10:14:49 +0200 Lars Noschinski merged
Wed, 22 Sep 2010 09:56:39 +0200 Lars Noschinski Remove unnecessary premise of mult1_union
Wed, 27 Oct 2010 16:40:31 +0200 haftmann sorting: avoid _key suffix if lemma applies both to simple and generalized variant; generalized insort_insert to insort_insert_key; additional lemmas
Fri, 17 Sep 2010 20:53:50 +0200 haftmann generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
Tue, 14 Sep 2010 08:40:22 +0200 nipkow removed duplicate lemma
Mon, 13 Sep 2010 11:13:15 +0200 nipkow renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
less more (0) -100 -60 tip