| Wed, 11 Feb 2015 15:03:21 +0100 |
Andreas Lochbihler |
more transfer rules
|
file |
diff |
annotate
|
| Wed, 11 Feb 2015 14:45:10 +0100 |
Andreas Lochbihler |
add lemmas about functions on option
|
file |
diff |
annotate
|
| Wed, 11 Feb 2015 14:19:46 +0100 |
Andreas Lochbihler |
tuned proof
|
file |
diff |
annotate
|
| Fri, 07 Nov 2014 11:28:37 +0100 |
traytel |
more complete fp_sugars for sum and prod;
|
file |
diff |
annotate
|
| Tue, 04 Nov 2014 17:33:08 +0100 |
lammich |
Added Option.bind_split{,_asm,s}
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Thu, 11 Sep 2014 19:32:36 +0200 |
blanchet |
updated news
|
file |
diff |
annotate
|
| Wed, 03 Sep 2014 00:06:26 +0200 |
blanchet |
tuned imports
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 16:34:40 +0200 |
blanchet |
renamed BNF theories
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 16:17:46 +0200 |
blanchet |
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
|
file |
diff |
annotate
|
| Fri, 30 May 2014 12:27:51 +0200 |
blanchet |
tuned whitespace, to make datatype definitions slightly less intimidating
|
file |
diff |
annotate
|
| Mon, 26 May 2014 16:32:55 +0200 |
blanchet |
got rid of '=:' squiggly
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
rationalized internals
|
file |
diff |
annotate
|
| Mon, 17 Feb 2014 13:31:42 +0100 |
blanchet |
renamed 'datatype_new_compat' to 'datatype_compat'
|
file |
diff |
annotate
|
| Sun, 16 Feb 2014 18:39:40 +0100 |
blanchet |
folded 'Option.set' into BNF-generated 'set_option'
|
file |
diff |
annotate
|
| Fri, 14 Feb 2014 07:53:46 +0100 |
blanchet |
renamed 'enriched_type' to more informative 'functor' (following the renaming of enriched type constructors to bounded natural functors)
|
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 17:35:59 +0100 |
blanchet |
tuning
|
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 |
compatibility names
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
use new selector support to define 'the', 'hd', 'tl'
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
transformed 'option' and 'list' into new-style datatypes (but register them as old-style as well)
|
file |
diff |
annotate
|
| Fri, 24 Jan 2014 11:51:45 +0100 |
blanchet |
killed 'More_BNFs' by moving its various bits where they (now) belong
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 23:34:26 +0100 |
blanchet |
swapped dependencies of 'Finite_Set' and 'Option' (to move BNF up)
|
file |
diff |
annotate
|
| Thu, 26 Sep 2013 13:37:33 +0200 |
lammich |
Added symmetric code_unfold-lemmas for null and is_none
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 15:59:22 +0200 |
kuncar |
move useful lemmas to Main
|
file |
diff |
annotate
|
| Sun, 23 Jun 2013 21:16:07 +0200 |
haftmann |
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
|
file |
diff |
annotate
|
| Fri, 12 Apr 2013 17:21:51 +0200 |
wenzelm |
modifiers for classical wrappers operate on Proof.context instead of claset;
|
file |
diff |
annotate
|
| Wed, 13 Feb 2013 13:38:52 +0100 |
haftmann |
combinator List.those;
|
file |
diff |
annotate
|