| Mon, 01 Aug 2016 22:11:29 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Tue, 05 Jul 2016 23:39:49 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Mon, 07 Dec 2015 10:38:04 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Tue, 01 Sep 2015 22:32:58 +0200 |
wenzelm |
eliminated \<Colon>;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 22:58:50 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Thu, 11 Sep 2014 18:54:36 +0200 |
blanchet |
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
|
file |
diff |
annotate
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
added 'plugins' option to control which hooks are enabled
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 13:36:15 +0100 |
blanchet |
renamed 'map_sum' to 'sum_map'
|
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
|
| Wed, 19 Feb 2014 08:34:33 +0100 |
blanchet |
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
|
file |
diff |
annotate
|
| Mon, 17 Feb 2014 13:31:42 +0100 |
blanchet |
renamed old 'primrec' to 'old_primrec' (until the new 'primrec' can be moved above 'Nat' in the theory dependencies)
|
file |
diff |
annotate
|
| Fri, 14 Feb 2014 07:53:46 +0100 |
blanchet |
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
|
file |
diff |
annotate
|
| Fri, 14 Feb 2014 07:53:46 +0100 |
blanchet |
renamed 'wrap_free_constructors' to 'free_constructors' (cf. 'functor', 'bnf', etc.)
|
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
|
| Wed, 12 Feb 2014 17:35:59 +0100 |
blanchet |
tuning
|
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 duplicate 'case' definitions by first looking up 'Ctr_Sugar'
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 15:59:22 +0200 |
kuncar |
move useful lemmas to Main
|
file |
diff |
annotate
|
| Sat, 20 Oct 2012 09:12:16 +0200 |
haftmann |
moved quite generic material from theory Enum to more appropriate places
|
file |
diff |
annotate
|
| Fri, 12 Oct 2012 18:58:20 +0200 |
wenzelm |
discontinued obsolete typedef (open) syntax;
|
file |
diff |
annotate
|
| Wed, 30 Nov 2011 16:27:10 +0100 |
wenzelm |
prefer typedef without extra definition and alternative name;
|
file |
diff |
annotate
|
| Tue, 18 Oct 2011 15:19:06 +0200 |
huffman |
hide typedef-generated constants Product_Type.prod and Sum_Type.sum
|
file |
diff |
annotate
|
| Tue, 11 Jan 2011 14:12:37 +0100 |
haftmann |
"enriched_type" replaces less specific "type_lifting"
|
file |
diff |
annotate
|
| Tue, 21 Dec 2010 17:52:23 +0100 |
haftmann |
tuned type_lifting declarations
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 09:19:10 +0100 |
haftmann |
replace `type_mapper` by the more adequate `type_lifting`
|
file |
diff |
annotate
|
| Thu, 18 Nov 2010 17:01:16 +0100 |
haftmann |
mapper for sum type
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 17:25:22 +0200 |
nipkow |
hide Sum_Type.Plus
|
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
|