Thu, 04 Apr 2013 22:46:14 +0200 |
haftmann |
sup on multisets
|
file |
diff |
annotate
|
Wed, 03 Apr 2013 22:26:04 +0200 |
haftmann |
default implementation of multisets by list with reasonable coverage of operations on multisets
|
file |
diff |
annotate
|
Wed, 03 Apr 2013 22:26:04 +0200 |
haftmann |
optionalized very specific code setup for multisets
|
file |
diff |
annotate
|
Wed, 27 Mar 2013 10:55:05 +0100 |
haftmann |
centralized various multiset operations in theory multiset;
|
file |
diff |
annotate
|
Fri, 15 Feb 2013 11:47:34 +0100 |
haftmann |
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
|
file |
diff |
annotate
|
Fri, 15 Feb 2013 08:31:31 +0100 |
haftmann |
two target language numeral types: integer and natural, as replacement for code_numeral;
|
file |
diff |
annotate
|
Thu, 14 Feb 2013 15:27:10 +0100 |
haftmann |
reform of predicate compiler / quickcheck theories:
|
file |
diff |
annotate
|
Fri, 12 Oct 2012 18:58:20 +0200 |
wenzelm |
discontinued obsolete typedef (open) syntax;
|
file |
diff |
annotate
|
Thu, 11 Oct 2012 11:56:43 +0200 |
haftmann |
avoid global interpretation
|
file |
diff |
annotate
|
Thu, 11 Oct 2012 11:56:42 +0200 |
haftmann |
simplified construction of fold combinator on multisets;
|
file |
diff |
annotate
|
Thu, 04 Oct 2012 23:19:02 +0200 |
haftmann |
default simp rule for image under identity
|
file |
diff |
annotate
|
Sun, 16 Sep 2012 06:51:36 +0200 |
bulwahn |
removing find_theorems commands that were left in the developments accidently
|
file |
diff |
annotate
|
Sat, 15 Sep 2012 20:14:29 +0200 |
haftmann |
typeclass formalising bounded subtraction
|
file |
diff |
annotate
|
Tue, 29 May 2012 17:53:43 +0200 |
huffman |
add lemma set_of_image_mset
|
file |
diff |
annotate
|
Tue, 29 May 2012 17:06:04 +0200 |
huffman |
reordered sections
|
file |
diff |
annotate
|
Tue, 29 May 2012 11:41:37 +0200 |
huffman |
shortened yet more multiset proofs;
|
file |
diff |
annotate
|
Tue, 29 May 2012 11:30:13 +0200 |
huffman |
remove unused intermediate lemma
|
file |
diff |
annotate
|
Tue, 29 May 2012 11:13:00 +0200 |
huffman |
shortened more multiset proofs
|
file |
diff |
annotate
|
Tue, 29 May 2012 10:30:47 +0200 |
huffman |
shortened some proofs
|
file |
diff |
annotate
|
Tue, 29 May 2012 10:08:31 +0200 |
huffman |
use transfer method for instance proof
|
file |
diff |
annotate
|
Thu, 12 Apr 2012 10:13:33 +0200 |
bulwahn |
multiset operations are defined with lift_definitions;
|
file |
diff |
annotate
|
Tue, 03 Apr 2012 16:26:48 +0200 |
kuncar |
new package Lifting - initial commit
|
file |
diff |
annotate
|
Thu, 29 Mar 2012 21:13:48 +0200 |
kuncar |
use qualified names for rsp and rep_eq theorems in quotient_def
|
file |
diff |
annotate
|
Wed, 28 Mar 2012 10:16:02 +0200 |
bulwahn |
changing more definitions to quotient_definition
|
file |
diff |
annotate
|
Wed, 28 Mar 2012 10:00:52 +0200 |
bulwahn |
using abstract code equations for proofs of code equations in Multiset
|
file |
diff |
annotate
|
Tue, 27 Mar 2012 14:14:46 +0200 |
bulwahn |
association lists with distinct keys uses the quotient infrastructure to obtain code certificates;
|
file |
diff |
annotate
|
Wed, 14 Mar 2012 15:59:39 +0100 |
wenzelm |
some proof indentation;
|
file |
diff |
annotate
|
Fri, 02 Mar 2012 09:35:32 +0100 |
bulwahn |
adding finiteness of intervals on integer sets; adding another finiteness theorem for multisets
|
file |
diff |
annotate
|
Tue, 28 Feb 2012 20:20:09 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
Wed, 01 Feb 2012 15:28:02 +0100 |
bulwahn |
improving code equations for multisets that violated the distinct AList abstraction
|
file |
diff |
annotate
|
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)
|
file |
diff |
annotate
|
Tue, 17 Jan 2012 09:38:30 +0100 |
bulwahn |
renamed theory AList to DAList
|
file |
diff |
annotate
|
Tue, 10 Jan 2012 10:17:09 +0100 |
bulwahn |
improving code generation for multisets; adding exhaustive quickcheck generators for multisets
|
file |
diff |
annotate
|
Mon, 26 Dec 2011 22:17:10 +0100 |
haftmann |
moved theorem requiring multisets from More_List to Multiset
|
file |
diff |
annotate
|
Wed, 14 Dec 2011 15:56:29 +0100 |
bulwahn |
adding code attribute to enable evaluation of equality on multisets
|
file |
diff |
annotate
|
Wed, 30 Nov 2011 16:27:10 +0100 |
wenzelm |
prefer typedef without extra definition and alternative name;
|
file |
diff |
annotate
|
Sun, 20 Nov 2011 21:28:07 +0100 |
wenzelm |
eliminated obsolete "standard";
|
file |
diff |
annotate
|
Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
Sat, 20 Aug 2011 23:36:18 +0200 |
wenzelm |
odd workaround for odd problem of load order in HOL/ex/ROOT.ML (!??);
|
file |
diff |
annotate
|
Fri, 20 May 2011 11:44:16 +0200 |
haftmann |
names of fold_set locales resemble name of characteristic property more closely
|
file |
diff |
annotate
|
Sat, 14 May 2011 18:26:25 +0200 |
haftmann |
use pointfree characterisation for fold_set locale
|
file |
diff |
annotate
|
Tue, 11 Jan 2011 14:12:37 +0100 |
haftmann |
"enriched_type" replaces less specific "type_lifting"
|
file |
diff |
annotate
|
Tue, 21 Dec 2010 17:52:23 +0100 |
haftmann |
tuned type_lifting declarations
|
file |
diff |
annotate
|
Tue, 07 Dec 2010 16:33:54 +0100 |
haftmann |
name filter operation just filter (c.f. List.filter and list comprehension syntax)
|
file |
diff |
annotate
|
Mon, 06 Dec 2010 09:19:10 +0100 |
haftmann |
replace `type_mapper` by the more adequate `type_lifting`
|
file |
diff |
annotate
|
Fri, 03 Dec 2010 22:34:20 +0100 |
haftmann |
lemma multiset_of_rev
|
file |
diff |
annotate
|
Thu, 18 Nov 2010 17:01:16 +0100 |
haftmann |
mapper for mulitset type
|
file |
diff |
annotate
|
Wed, 03 Nov 2010 12:15:47 +0100 |
haftmann |
added code lemmas for stable parametrized quicksort
|
file |
diff |
annotate
|
Wed, 03 Nov 2010 11:50:29 +0100 |
haftmann |
tuned proof
|
file |
diff |
annotate
|
Tue, 02 Nov 2010 16:59:40 +0100 |
haftmann |
tuned proof
|
file |
diff |
annotate
|
Tue, 02 Nov 2010 16:48:19 +0100 |
haftmann |
tuned proof
|
file |
diff |
annotate
|
Tue, 02 Nov 2010 16:36:33 +0100 |
haftmann |
tuned lemma proposition of properties_for_sort_key
|
file |
diff |
annotate
|
Tue, 02 Nov 2010 16:31:56 +0100 |
haftmann |
lemmas multiset_of_filter, sort_key_by_quicksort
|
file |
diff |
annotate
|
Fri, 29 Oct 2010 10:14:49 +0200 |
Lars Noschinski |
merged
|
file |
diff |
annotate
|
Wed, 22 Sep 2010 09:56:39 +0200 |
Lars Noschinski |
Remove unnecessary premise of mult1_union
|
file |
diff |
annotate
|
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
|
file |
diff |
annotate
|
Fri, 17 Sep 2010 20:53:50 +0200 |
haftmann |
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
|
file |
diff |
annotate
|
Tue, 14 Sep 2010 08:40:22 +0200 |
nipkow |
removed duplicate lemma
|
file |
diff |
annotate
|
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
|
file |
diff |
annotate
|
Mon, 13 Sep 2010 08:43:48 +0200 |
nipkow |
added and renamed lemmas
|
file |
diff |
annotate
|
Tue, 07 Sep 2010 10:05:19 +0200 |
nipkow |
expand_fun_eq -> ext_iff
|
file |
diff |
annotate
|
Fri, 27 Aug 2010 19:34:23 +0200 |
haftmann |
renamed class/constant eq to equal; tuned some instantiations
|
file |
diff |
annotate
|
Mon, 09 Aug 2010 12:53:16 +0200 |
blanchet |
replace "setup" with "declaration"
|
file |
diff |
annotate
|
Fri, 06 Aug 2010 17:23:11 +0200 |
blanchet |
adapt occurrences of renamed Nitpick functions
|
file |
diff |
annotate
|
Mon, 12 Jul 2010 08:58:13 +0200 |
haftmann |
dropped superfluous [code del]s
|
file |
diff |
annotate
|
Fri, 09 Jul 2010 08:11:10 +0200 |
haftmann |
nicer xsymbol syntax for fcomp and scomp
|
file |
diff |
annotate
|
Tue, 01 Jun 2010 14:14:02 +0200 |
blanchet |
honor xsymbols in Nitpick
|
file |
diff |
annotate
|
Thu, 27 May 2010 16:42:03 +0200 |
blanchet |
make Nitpick "show_all" option behave less surprisingly
|
file |
diff |
annotate
|
Mon, 24 May 2010 13:48:57 +0200 |
haftmann |
more lemmas
|
file |
diff |
annotate
|
Sat, 22 May 2010 10:12:49 +0200 |
haftmann |
localized properties_for_sort
|
file |
diff |
annotate
|
Thu, 13 May 2010 14:34:05 +0200 |
nipkow |
Multiset: renamed, added and tuned lemmas;
|
file |
diff |
annotate
|
Wed, 12 May 2010 15:25:02 +0200 |
nipkow |
simplified proof
|
file |
diff |
annotate
|
Tue, 04 May 2010 08:55:43 +0200 |
haftmann |
locale predicates of classes carry a mandatory "class" prefix
|
file |
diff |
annotate
|
Fri, 16 Apr 2010 21:28:09 +0200 |
wenzelm |
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
|
file |
diff |
annotate
|
Thu, 11 Mar 2010 15:33:45 +0100 |
blanchet |
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
|
file |
diff |
annotate
|
Sat, 27 Feb 2010 20:57:08 +0100 |
wenzelm |
clarified @{const_name} vs. @{const_abbrev};
|
file |
diff |
annotate
|
Wed, 24 Feb 2010 21:55:46 +0100 |
wenzelm |
observe standard convention for syntax consts;
|
file |
diff |
annotate
|
Tue, 23 Feb 2010 08:08:23 +0100 |
haftmann |
mind the "s"
|
file |
diff |
annotate
|
Mon, 22 Feb 2010 09:15:11 +0100 |
haftmann |
ascii syntax for multiset order
|
file |
diff |
annotate
|
Fri, 19 Feb 2010 16:52:00 +0100 |
haftmann |
switched notations for pointwise and multiset order
|
file |
diff |
annotate
|
Fri, 05 Feb 2010 14:33:50 +0100 |
haftmann |
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
|
file |
diff |
annotate
|
Fri, 22 Jan 2010 13:38:28 +0100 |
haftmann |
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
|
file |
diff |
annotate
|
Sun, 25 Oct 2009 00:00:53 +0200 |
wenzelm |
adapted Function_Lib (cf. b8cdd3d73022);
|
file |
diff |
annotate
|
Sat, 17 Oct 2009 14:43:18 +0200 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
Fri, 28 Aug 2009 19:35:49 +0200 |
nipkow |
tuned proofs
|
file |
diff |
annotate
|
Thu, 26 Mar 2009 20:08:55 +0100 |
wenzelm |
interpretation/interpret: prefixes are mandatory by default;
|
file |
diff |
annotate
|
Mon, 23 Mar 2009 08:14:24 +0100 |
haftmann |
Main is (Complex_Main) base entry point in library theories
|
file |
diff |
annotate
|
Thu, 19 Mar 2009 22:05:00 +0100 |
wenzelm |
proper spacing before ML antiquotations -- note that @ may be part of symbolic ML identifiers;
|
file |
diff |
annotate
|
Wed, 11 Mar 2009 08:45:46 +0100 |
haftmann |
explicitly delete some code equations
|
file |
diff |
annotate
|
Fri, 13 Feb 2009 23:55:04 +0100 |
nipkow |
finiteness lemmas
|
file |
diff |
annotate
|
Fri, 16 Jan 2009 14:58:11 +0100 |
haftmann |
migrated class package to new locale implementation
|
file |
diff |
annotate
|
Tue, 30 Dec 2008 11:10:01 +0100 |
ballarin |
Merged.
|
file |
diff |
annotate
|
Sun, 14 Dec 2008 18:45:51 +0100 |
ballarin |
Ported HOL and HOL-Library to new locales.
|
file |
diff |
annotate
|
Tue, 16 Dec 2008 08:46:07 +0100 |
krauss |
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
|
file |
diff |
annotate
|
Mon, 17 Nov 2008 17:00:55 +0100 |
haftmann |
tuned unfold_locales invocation
|
file |
diff |
annotate
|
Wed, 29 Oct 2008 11:33:40 +0100 |
haftmann |
explicit check for pattern discipline before code translation
|
file |
diff |
annotate
|
Fri, 10 Oct 2008 06:45:53 +0200 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
Fri, 25 Jul 2008 12:03:34 +0200 |
haftmann |
added class preorder
|
file |
diff |
annotate
|
Tue, 15 Jul 2008 16:50:09 +0200 |
ballarin |
Removed uses of context element includes.
|
file |
diff |
annotate
|
Mon, 07 Jul 2008 08:47:17 +0200 |
haftmann |
absolute imports of HOL/*.thy theories
|
file |
diff |
annotate
|
Thu, 26 Jun 2008 10:07:01 +0200 |
haftmann |
established Plain theory and image
|
file |
diff |
annotate
|
Tue, 10 Jun 2008 15:30:56 +0200 |
haftmann |
removed some dubious code lemmas
|
file |
diff |
annotate
|
Wed, 07 May 2008 10:59:33 +0200 |
berghofe |
Instantiated rule expand_fun_eq in proof of set_of_eq_empty_iff, to avoid that
|
file |
diff |
annotate
|
Mon, 07 Apr 2008 15:37:34 +0200 |
haftmann |
instantiation replacing primitive instance plus overloaded defs; more conservative type arities
|
file |
diff |
annotate
|
Thu, 28 Feb 2008 14:04:29 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
Thu, 28 Feb 2008 12:56:31 +0100 |
wenzelm |
tuned syntax declaration;
|
file |
diff |
annotate
|
Tue, 26 Feb 2008 16:10:54 +0100 |
wenzelm |
tuned document;
|
file |
diff |
annotate
|
Tue, 26 Feb 2008 11:18:43 +0100 |
bulwahn |
Added useful general lemmas from the work with the HeapMonad
|
file |
diff |
annotate
|
Fri, 01 Feb 2008 18:01:06 +0100 |
nipkow |
modified MCollect syntax
|
file |
diff |
annotate
|
Wed, 30 Jan 2008 17:34:21 +0100 |
nipkow |
added multiset comprehension
|
file |
diff |
annotate
|
Wed, 02 Jan 2008 04:10:47 +0100 |
kleing |
renamed foldM to fold_mset on general request
|
file |
diff |
annotate
|
Thu, 13 Dec 2007 22:35:45 +0100 |
kleing |
removed syntax in locale left_commutative
|
file |
diff |
annotate
|
Thu, 13 Dec 2007 07:09:23 +0100 |
haftmann |
changed order in class parameters
|
file |
diff |
annotate
|
Thu, 13 Dec 2007 06:51:22 +0100 |
kleing |
a fold operation for multisets + more lemmas
|
file |
diff |
annotate
|
Mon, 10 Dec 2007 11:24:12 +0100 |
haftmann |
switched import from Main to List
|
file |
diff |
annotate
|
Fri, 07 Dec 2007 15:07:59 +0100 |
haftmann |
instantiation target rather than legacy instance
|
file |
diff |
annotate
|
Fri, 30 Nov 2007 11:51:22 +0100 |
nipkow |
added {#.,.,...#}
|
file |
diff |
annotate
|
Fri, 26 Oct 2007 21:22:19 +0200 |
haftmann |
changed order of class parameters
|
file |
diff |
annotate
|
Tue, 23 Oct 2007 23:27:23 +0200 |
nipkow |
went back to >0
|
file |
diff |
annotate
|
Sun, 21 Oct 2007 22:33:35 +0200 |
nipkow |
More changes from >0 to ~=0::nat
|
file |
diff |
annotate
|