| Sun, 21 Aug 2022 06:18:23 +0000 |
haftmann |
streamlined
|
file |
diff |
annotate
|
| Wed, 31 Mar 2021 18:18:03 +0200 |
nipkow |
new automatic order prover: stateless, complete, verified
|
file |
diff |
annotate
|
| Sun, 31 Jan 2021 08:49:47 +0100 |
Andreas Lochbihler |
hide the internal abbreviations MR and MB
|
file |
diff |
annotate
|
| Fri, 29 Jan 2021 13:06:29 +0100 |
mraszyk |
optimize RBT_Impl
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Fri, 15 Jun 2018 10:45:12 +0200 |
nipkow |
Map.empty now qualified to avoid name clashes
|
file |
diff |
annotate
|
| Tue, 08 May 2018 10:14:36 +0200 |
nipkow |
new def of sorted and sorted_wrt
|
file |
diff |
annotate
|
| Fri, 12 Jan 2018 15:27:46 +0100 |
wenzelm |
prefer formal comments;
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:21 +0200 |
haftmann |
elementary definition of division on natural numbers
|
file |
diff |
annotate
|
| Sun, 16 Oct 2016 09:31:06 +0200 |
haftmann |
eliminated irregular aliasses
|
file |
diff |
annotate
|
| Sun, 16 Oct 2016 09:31:05 +0200 |
haftmann |
eliminated irregular aliasses
|
file |
diff |
annotate
|
| Fri, 12 Aug 2016 17:53:55 +0200 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Wed, 10 Aug 2016 14:50:59 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Mon, 25 Apr 2016 16:09:26 +0200 |
wenzelm |
eliminated old 'def';
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 16:25:08 +0100 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
| Thu, 07 Jan 2016 15:53:39 +0100 |
wenzelm |
more uniform treatment of package internals;
|
file |
diff |
annotate
|
| Thu, 05 Nov 2015 10:39:49 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Sat, 17 Oct 2015 13:18:43 +0200 |
haftmann |
qualify some names stemming from internal bootstrap constructions
|
file |
diff |
annotate
|
| Tue, 22 Sep 2015 14:31:22 +0200 |
nipkow |
tuned references
|
file |
diff |
annotate
|
| Sun, 06 Sep 2015 21:55:13 +0200 |
wenzelm |
do not expose low-level "_def" facts of 'function' definitions, to avoid potential confusion with the situation of plain 'definition';
|
file |
diff |
annotate
|
| Tue, 01 Sep 2015 22:32:58 +0200 |
wenzelm |
eliminated \<Colon>;
|
file |
diff |
annotate
|
| Wed, 17 Jun 2015 11:03:05 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Tue, 03 Mar 2015 16:37:45 +0100 |
blanchet |
removed needless (and inconsistent) qualifier that messes up with Mirabelle
|
file |
diff |
annotate
|
| Wed, 18 Feb 2015 22:46:47 +0100 |
haftmann |
inlined rules to free user-space from technical names
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 17:20:45 +0100 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
| Thu, 11 Sep 2014 19:32:36 +0200 |
blanchet |
updated news
|
file |
diff |
annotate
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
half-ported Imperative HOL to new datatypes
|
file |
diff |
annotate
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
|
file |
diff |
annotate
|
| Mon, 18 Aug 2014 17:19:58 +0200 |
blanchet |
reordered some (co)datatype property names for more consistency
|
file |
diff |
annotate
|
| Fri, 04 Jul 2014 20:18:47 +0200 |
haftmann |
reduced name variants for assoc and commute on plus and mult
|
file |
diff |
annotate
|
| Fri, 21 Feb 2014 00:09:56 +0100 |
blanchet |
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
|
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:37:06 +0100 |
blanchet |
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
renamed '{prod,sum,bool,unit}_case' to 'case_...'
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
avoid old 'prod.simps' -- better be more specific
|
file |
diff |
annotate
|
| Tue, 03 Sep 2013 01:12:40 +0200 |
wenzelm |
tuned proofs -- clarified flow of facts wrt. calculation;
|
file |
diff |
annotate
|
| Wed, 10 Oct 2012 16:18:27 +0200 |
Andreas Lochbihler |
fix code equation for RBT_Impl.fold
|
file |
diff |
annotate
|
| Wed, 10 Oct 2012 15:05:07 +0200 |
Andreas Lochbihler |
correct definition for skip_black
|
file |
diff |
annotate
|
| Wed, 10 Oct 2012 13:03:50 +0200 |
Andreas Lochbihler |
efficient construction of red black trees from sorted associative lists
|
file |
diff |
annotate
|
| Thu, 20 Sep 2012 17:17:20 +0200 |
Andreas Lochbihler |
more efficient code setup
|
file |
diff |
annotate
|
| Tue, 31 Jul 2012 13:55:39 +0200 |
kuncar |
a couple of additions to RBT formalization to allow us to implement RBT_Set
|
file |
diff |
annotate
|
| Fri, 13 Apr 2012 14:00:26 +0200 |
wenzelm |
updated headers;
|
file |
diff |
annotate
|
| Fri, 13 Apr 2012 11:45:30 +0200 |
Andreas Lochbihler |
move RBT implementation into type class contexts
|
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
|
| Fri, 06 Jan 2012 10:19:49 +0100 |
haftmann |
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
|
file |
diff |
annotate
|
| Mon, 26 Dec 2011 22:17:10 +0100 |
haftmann |
incorporated More_Set and More_List into the Main body -- to be consolidated later
|
file |
diff |
annotate
|
| Sun, 13 Mar 2011 22:55:50 +0100 |
wenzelm |
tuned headers;
|
file |
diff |
annotate
|
| Wed, 08 Dec 2010 13:34:50 +0100 |
haftmann |
hide popular names R and B
|
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
|
| Mon, 28 Jun 2010 15:03:07 +0200 |
haftmann |
merged constants "split" and "prod_case"
|
file |
diff |
annotate
|
| Fri, 18 Jun 2010 15:03:20 +0200 |
haftmann |
prefer fold over foldl
|
file |
diff |
annotate
|
| Fri, 16 Apr 2010 21:28:09 +0200 |
wenzelm |
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
|
file |
diff |
annotate
|
| Thu, 15 Apr 2010 12:27:14 +0200 |
haftmann |
theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
|
file |
diff |
annotate
| base
|