| Tue, 01 Jun 2021 19:46:34 +0200 |
nipkow |
More general fold function for maps
|
file |
diff |
annotate
|
| Wed, 12 May 2021 09:31:18 +0200 |
desharna |
added lemmas map_ran_Cons_sel and (length|map_fst)_map_ran
|
file |
diff |
annotate
|
| Tue, 11 May 2021 22:40:59 +0200 |
nipkow |
generalized type
|
file |
diff |
annotate
|
| Mon, 14 Jan 2019 18:35:03 +0000 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Wed, 06 Jun 2018 11:12:37 +0200 |
nipkow |
Keep filter input syntax
|
file |
diff |
annotate
|
| Tue, 22 May 2018 11:08:37 +0200 |
nipkow |
First step to remove nonstandard "[x <- xs. P]" syntax: only input
|
file |
diff |
annotate
|
| Wed, 13 Jul 2016 19:02:23 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 12 Jul 2016 15:45:32 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 16:25:08 +0100 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
| Thu, 05 Nov 2015 10:39:49 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Wed, 17 Jun 2015 11:03:05 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Mon, 13 Apr 2015 10:36:06 +0200 |
nipkow |
moved _aux functions from AFP/Collections to AList
|
file |
diff |
annotate
|
| Thu, 09 Apr 2015 20:42:32 +0200 |
wenzelm |
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
|
file |
diff |
annotate
|
| Tue, 07 Apr 2015 10:13:33 +0200 |
wenzelm |
more qualified names -- eliminated hide_const (open);
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 17:20:45 +0100 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
| Sun, 30 Mar 2014 21:24:59 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Fri, 14 Feb 2014 07:53:46 +0100 |
blanchet |
merged 'Option.map' and 'Option.map_option'
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
renamed '{prod,sum,bool,unit}_case' to 'case_...'
|
file |
diff |
annotate
|
| Fri, 06 Apr 2012 18:17:16 +0200 |
haftmann |
no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
|
file |
diff |
annotate
|
| Thu, 16 Feb 2012 22:53:24 +0100 |
wenzelm |
tuned proofs;
|
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
| base
|
| Tue, 10 Jan 2012 15:48:10 +0100 |
bulwahn |
proper hiding of facts and constants in AList_Impl and AList theory
|
file |
diff |
annotate
|
| Tue, 10 Jan 2012 10:17:07 +0100 |
bulwahn |
adding theory association lists with invariant
|
file |
diff |
annotate
|
| Wed, 14 Dec 2011 15:56:37 +0100 |
bulwahn |
adding map_entry to AList theory
|
file |
diff |
annotate
|
| Wed, 14 Dec 2011 15:56:34 +0100 |
bulwahn |
adding map_default to AList theory
|
file |
diff |
annotate
|
| Wed, 14 Dec 2011 15:56:31 +0100 |
bulwahn |
fixed typo in theorem name in AList theory
|
file |
diff |
annotate
|
| Sun, 20 Nov 2011 21:05:23 +0100 |
wenzelm |
eliminated obsolete "standard";
|
file |
diff |
annotate
|
| Tue, 13 Sep 2011 09:28:03 +0200 |
bulwahn |
correcting theory name and dependencies
|
file |
diff |
annotate
|
| Tue, 13 Sep 2011 09:25:19 +0200 |
bulwahn |
renamed AList_Impl to AList
|
file |
diff |
annotate
| base
|