| Fri, 04 Jul 2014 20:18:47 +0200 |
haftmann |
reduced name variants for assoc and commute on plus and mult
|
file |
diff |
annotate
|
| Wed, 11 Jun 2014 14:24:23 +1000 |
Thomas Sewell |
Hypsubst preserves equality hypotheses
|
file |
diff |
annotate
|
| Sat, 28 Jun 2014 09:16:42 +0200 |
haftmann |
fact consolidation
|
file |
diff |
annotate
|
| Wed, 23 Apr 2014 10:23:27 +0200 |
blanchet |
size function for multisets
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 15:40:33 +0100 |
blanchet |
renamed 'fun_rel' to 'rel_fun'
|
file |
diff |
annotate
|
| Wed, 05 Mar 2014 09:59:48 +0100 |
wenzelm |
proper UTF-8;
|
file |
diff |
annotate
|
| Fri, 28 Feb 2014 17:54:52 +0100 |
traytel |
load Metis a little later
|
file |
diff |
annotate
|
| Fri, 28 Feb 2014 18:11:02 +0100 |
nipkow |
added Rene Thiemann's patch for the nonterminating equality/subset test code for multisets
|
file |
diff |
annotate
|
| Tue, 18 Feb 2014 23:03:50 +0100 |
kuncar |
simplify proofs because of the stronger reflexivity prover
|
file |
diff |
annotate
|
| Fri, 14 Feb 2014 07:53:46 +0100 |
blanchet |
renamed 'enriched_type' to more informative 'functor' (following the renaming of enriched type constructors to bounded natural functors)
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:37:06 +0100 |
blanchet |
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
|
file |
diff |
annotate
|
| Fri, 24 Jan 2014 11:51:45 +0100 |
blanchet |
killed 'More_BNFs' by moving its various bits where they (now) belong
|
file |
diff |
annotate
|
| Fri, 27 Dec 2013 14:35:14 +0100 |
haftmann |
prefer target-style syntaxx for sublocale
|
file |
diff |
annotate
|
| Sun, 10 Nov 2013 15:05:06 +0100 |
haftmann |
qualifed popular user space names
|
file |
diff |
annotate
|
| Sun, 02 Jun 2013 20:44:55 +0200 |
haftmann |
type class for confined subtraction
|
file |
diff |
annotate
|
| 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
|