| Tue, 09 Oct 2012 16:57:58 +0200 |
kuncar |
rename Set.project to Set.filter - more appropriate name
|
file |
diff |
annotate
|
| Wed, 10 Oct 2012 15:39:01 +0200 |
wenzelm |
added some ad-hoc namespace prefixes to avoid duplicate facts;
|
file |
diff |
annotate
|
| Mon, 08 Oct 2012 12:03:49 +0200 |
haftmann |
consolidated names of theorems on composition;
|
file |
diff |
annotate
|
| Sat, 06 Oct 2012 16:03:41 +0200 |
haftmann |
congruence rule for Finite_Set.fold
|
file |
diff |
annotate
|
| Sat, 06 Oct 2012 11:08:52 +0200 |
haftmann |
alternative simplification of ^^ to the righthand side;
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 22:55:41 +0200 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
| Wed, 01 Aug 2012 15:32:36 +0200 |
wenzelm |
removed junk;
|
file |
diff |
annotate
|
| Tue, 31 Jul 2012 13:55:39 +0200 |
kuncar |
more set operations expressed by Finite_Set.fold
|
file |
diff |
annotate
|
| Tue, 03 Jul 2012 09:25:42 +0200 |
Andreas Lochbihler |
add finiteness lemmas for 'a * 'b and 'a set
|
file |
diff |
annotate
|
| Mon, 25 Jun 2012 18:21:18 +0200 |
wenzelm |
merged, resolving conflict with 87c831e30f0a;
|
file |
diff |
annotate
|
| Mon, 25 Jun 2012 17:41:20 +0200 |
wenzelm |
tuned proofs -- prefer direct "rotated" instead of old-style COMP;
|
file |
diff |
annotate
|
| Mon, 25 Jun 2012 15:14:07 +0200 |
wenzelm |
ignore morphism more explicitly;
|
file |
diff |
annotate
|
| Mon, 25 Jun 2012 16:03:14 +0200 |
bulwahn |
adding set comprehension simproc to code generation's preprocessing to generate code for some set comprehensions;
|
file |
diff |
annotate
|
| Wed, 20 Jun 2012 16:54:08 +0200 |
Rafal Kolanski |
Integrated set comprehension pointfree simproc.
|
file |
diff |
annotate
|
| Fri, 01 Jun 2012 11:53:58 +0200 |
huffman |
remove duplicate lemma card_unit in favor of Finite_Set.card_UNIV_unit
|
file |
diff |
annotate
|
| Fri, 30 Mar 2012 14:00:18 +0200 |
huffman |
rephrase lemma card_Pow using '2' instead of 'Suc (Suc 0)'
|
file |
diff |
annotate
|
| Fri, 30 Mar 2012 08:04:28 +0200 |
huffman |
move lemma card_UNIV_bool from Nat_Numeral.thy to Finite_Set.thy
|
file |
diff |
annotate
|
| Tue, 13 Mar 2012 13:31:26 +0100 |
wenzelm |
tuned proofs -- eliminated pointless chaining of facts after 'interpret';
|
file |
diff |
annotate
|
| Fri, 06 Jan 2012 21:48:45 +0100 |
haftmann |
incorporated various theorems from theory More_Set into corpus
|
file |
diff |
annotate
|
| Thu, 29 Dec 2011 13:41:41 +0100 |
haftmann |
qualified Finite_Set.fold
|
file |
diff |
annotate
|
| Sat, 24 Dec 2011 15:53:08 +0100 |
haftmann |
finite type class instance for `set`
|
file |
diff |
annotate
|
| Tue, 18 Oct 2011 15:27:18 +0200 |
bulwahn |
tuned
|
file |
diff |
annotate
|
| Wed, 14 Sep 2011 10:08:52 -0400 |
hoelzl |
renamed Complete_Lattices lemmas, removed legacy names
|
file |
diff |
annotate
|
| Tue, 13 Sep 2011 16:22:01 +0200 |
noschinl |
tune proofs
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
| Tue, 06 Sep 2011 22:04:14 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Mon, 05 Sep 2011 07:49:31 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Tue, 06 Sep 2011 14:25:16 +0200 |
nipkow |
added new lemmas
|
file |
diff |
annotate
|
| Wed, 27 Jul 2011 19:34:30 +0200 |
hoelzl |
finite vimage on arbitrary domains
|
file |
diff |
annotate
|
| Sun, 17 Jul 2011 19:48:02 +0200 |
haftmann |
moving UNIV = ... equations to their proper theories
|
file |
diff |
annotate
|
| Fri, 20 May 2011 12:35:44 +0200 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Fri, 20 May 2011 12:07:17 +0200 |
haftmann |
point-free characterization of operations on finite sets
|
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
|
| Fri, 20 May 2011 08:16:56 +0200 |
haftmann |
use point-free characterization for locale fun_left_comm_idem
|
file |
diff |
annotate
|
| Sat, 14 May 2011 18:26:25 +0200 |
haftmann |
use pointfree characterisation for fold_set locale
|
file |
diff |
annotate
|
| Thu, 12 May 2011 11:03:48 +0200 |
haftmann |
more uniform naming of lemma
|
file |
diff |
annotate
|
| Thu, 07 Apr 2011 13:01:27 +0200 |
haftmann |
dropped unused lemmas; proper Isar proof
|
file |
diff |
annotate
|
| Sun, 03 Apr 2011 11:40:32 +0200 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Sat, 02 Apr 2011 18:07:29 +0200 |
haftmann |
tuned proof
|
file |
diff |
annotate
|
| Thu, 17 Mar 2011 09:58:13 +0100 |
nipkow |
tuned lemma
|
file |
diff |
annotate
|
| Wed, 16 Mar 2011 19:50:56 +0100 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
| Fri, 21 Jan 2011 09:44:12 +0100 |
haftmann |
moved theorem
|
file |
diff |
annotate
|
| Fri, 21 Jan 2011 09:41:59 +0100 |
haftmann |
restructured theory;
|
file |
diff |
annotate
|
| Fri, 14 Jan 2011 15:44:47 +0100 |
wenzelm |
eliminated global prems;
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 20:38:58 +0100 |
wenzelm |
recoded latin1 as utf8;
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 08:40:47 +0100 |
bulwahn |
adding code equation for finiteness of finite types
|
file |
diff |
annotate
|
| Sun, 28 Nov 2010 15:20:51 +0100 |
nipkow |
gave more standard finite set rules simp and intro attribute
|
file |
diff |
annotate
|
| Fri, 26 Nov 2010 18:06:48 +0100 |
nipkow |
new lemma
|
file |
diff |
annotate
|
| Tue, 23 Nov 2010 14:14:17 +0100 |
hoelzl |
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
|
file |
diff |
annotate
|
| Mon, 22 Nov 2010 10:34:33 +0100 |
hoelzl |
Replace surj by abbreviation; remove surj_on.
|
file |
diff |
annotate
|
| Wed, 03 Nov 2010 08:29:32 +0100 |
nipkow |
removed assumption
|
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
|
| Tue, 07 Sep 2010 10:05:19 +0200 |
nipkow |
expand_fun_eq -> ext_iff
|
file |
diff |
annotate
|
| Fri, 13 Aug 2010 10:51:23 +0200 |
haftmann |
import swap prevents strange failure of SML code generator for datatypes
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 11:39:27 +0200 |
haftmann |
avoid explicit mandatory prefix markers when prefixes are mandatory implicitly
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 10:48:37 +0200 |
haftmann |
dropped superfluous [code del]s
|
file |
diff |
annotate
|
| Thu, 01 Jul 2010 16:54:44 +0200 |
haftmann |
"prod" and "sum" replace "*" and "+" respectively
|
file |
diff |
annotate
|
| Fri, 18 Jun 2010 22:40:58 +0200 |
nipkow |
added pigeonhole lemmas
|
file |
diff |
annotate
|
| Tue, 04 May 2010 10:02:43 +0200 |
haftmann |
avoid if on rhs of default simp rules
|
file |
diff |
annotate
|
| Tue, 04 May 2010 08:55:43 +0200 |
haftmann |
locale predicates of classes carry a mandatory "class" prefix
|
file |
diff |
annotate
|