| Wed, 05 Feb 2020 20:17:00 +0000 |
haftmann |
simplified logical constructions
|
file |
diff |
annotate
|
| Mon, 26 Feb 2018 11:52:53 +0000 |
haftmann |
new lemma
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Wed, 05 Apr 2017 13:47:38 +0200 |
haftmann |
more on lists
|
file |
diff |
annotate
|
| Fri, 22 Jul 2016 11:00:43 +0200 |
wenzelm |
tuned proofs -- avoid unstructured calculation;
|
file |
diff |
annotate
|
| Mon, 25 Apr 2016 16:09:26 +0200 |
wenzelm |
eliminated old 'def';
|
file |
diff |
annotate
|
| Wed, 17 Jun 2015 11:03:05 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 17:20:45 +0100 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
| Wed, 24 Sep 2014 19:11:21 +0200 |
haftmann |
added lemmas
|
file |
diff |
annotate
|
| Wed, 10 Sep 2014 22:52:46 +0200 |
haftmann |
more material on lists
|
file |
diff |
annotate
|
| Sun, 07 Sep 2014 09:49:05 +0200 |
haftmann |
explicit theory with additional, less commonly used list operations
|
file |
diff |
annotate
|
| Sat, 24 Dec 2011 15:53:11 +0100 |
haftmann |
moved `sublists` to theory Enum
|
file |
diff |
annotate
|
| Sat, 15 Oct 2011 00:18:00 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Fri, 14 Oct 2011 22:42:56 +0200 |
haftmann |
monadic bind
|
file |
diff |
annotate
|
| Fri, 14 Oct 2011 18:55:59 +0200 |
haftmann |
moved sublists to More_List.thy
|
file |
diff |
annotate
|
| Wed, 14 Sep 2011 10:08:52 -0400 |
hoelzl |
renamed Complete_Lattices lemmas, removed legacy names
|
file |
diff |
annotate
|
| Tue, 02 Aug 2011 10:36:50 +0200 |
krauss |
moved recdef package to HOL/Library/Old_Recdef.thy
|
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, 03 Dec 2010 22:39:34 +0100 |
haftmann |
tuned proposition
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 22:34:20 +0100 |
haftmann |
lemmas fold_remove1_split and fold_multiset_equiv
|
file |
diff |
annotate
|
| Tue, 05 Oct 2010 11:37:42 +0200 |
haftmann |
lemmas fold_commute and fold_commute_apply
|
file |
diff |
annotate
|
| Wed, 29 Sep 2010 15:28:29 +0200 |
haftmann |
redundancy check: drop trailing Var arguments (avoids eta problems with equations)
|
file |
diff |
annotate
|
| Wed, 29 Sep 2010 09:08:00 +0200 |
haftmann |
delete code lemma explicitly
|
file |
diff |
annotate
|
| Tue, 28 Sep 2010 15:21:45 +0200 |
haftmann |
lemma listsum_conv_fold
|
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
|
| Thu, 20 May 2010 17:35:02 +0200 |
haftmann |
proper document text
|
file |
diff |
annotate
|
| Thu, 20 May 2010 16:43:00 +0200 |
haftmann |
added More_List.thy explicitly
|
file |
diff |
annotate
|