| Thu, 16 Jan 2014 18:26:41 +0100 |
blanchet |
dissolved 'Fun_More_FP' (a BNF dependency)
|
file |
diff |
annotate
|
| Sat, 28 Dec 2013 17:51:54 +0100 |
haftmann |
prefix disambiguation
|
file |
diff |
annotate
|
| Thu, 26 Dec 2013 22:47:49 +0100 |
haftmann |
prefer ephemeral interpretation over interpretation in proof contexts;
|
file |
diff |
annotate
|
| Fri, 29 Nov 2013 08:26:45 +0100 |
traytel |
set_comprehension_pointfree simproc causes to many surprises if enabled by default
|
file |
diff |
annotate
|
| Sun, 24 Nov 2013 00:31:50 +0000 |
paulson |
polished some ancient proofs
|
file |
diff |
annotate
|
| Tue, 12 Nov 2013 19:28:54 +0100 |
hoelzl |
add finite_select_induct; move generic lemmas from MV_Analysis/Linear_Algebra to the HOL image
|
file |
diff |
annotate
|
| Fri, 18 Oct 2013 10:43:21 +0200 |
blanchet |
killed more "no_atp"s
|
file |
diff |
annotate
|
| Fri, 18 Oct 2013 10:43:20 +0200 |
blanchet |
killed most "no_atp", to make Sledgehammer more complete
|
file |
diff |
annotate
|
| Tue, 24 Sep 2013 13:35:27 +0200 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
| Tue, 03 Sep 2013 01:12:40 +0200 |
wenzelm |
tuned proofs -- clarified flow of facts wrt. calculation;
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 16:25:47 +0200 |
wenzelm |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
file |
diff |
annotate
|
| Thu, 04 Apr 2013 22:29:59 +0200 |
haftmann |
convenient induction rule
|
file |
diff |
annotate
|
| Wed, 03 Apr 2013 10:15:43 +0200 |
haftmann |
generalized lemma fold_image thanks to Peter Lammich
|
file |
diff |
annotate
|
| Tue, 26 Mar 2013 21:53:56 +0100 |
haftmann |
more uniform style for interpretation and sublocale declarations
|
file |
diff |
annotate
|
| Sat, 23 Mar 2013 20:50:39 +0100 |
haftmann |
fundamental revision of big operators on sets
|
file |
diff |
annotate
|
| Sat, 23 Mar 2013 17:11:06 +0100 |
haftmann |
locales for abstract orders
|
file |
diff |
annotate
|
| Wed, 27 Feb 2013 13:43:04 +0100 |
Andreas Lochbihler |
added lemma
|
file |
diff |
annotate
|
| Wed, 10 Oct 2012 16:19:52 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Wed, 10 Oct 2012 10:47:43 +0200 |
bulwahn |
moving simproc from Finite_Set to more appropriate Product_Type theory
|
file |
diff |
annotate
|
| Tue, 09 Oct 2012 16:58:36 +0200 |
kuncar |
use Set.filter instead of Finite_Set.filter, which is removed then
|
file |
diff |
annotate
|
| 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
|