| Tue, 09 Mar 2021 14:20:27 +0100 |
traytel |
generalized confluence-based subdistributivity theorem for quotients;
|
file |
diff |
annotate
|
| Fri, 28 Feb 2020 21:23:11 +0100 |
traytel |
tuned lift_bnf's user interface for quotients
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Mon, 04 Jul 2016 19:46:20 +0200 |
haftmann |
basic facts about almost everywhere fix bijections
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 16:25:08 +0100 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
| Tue, 16 Feb 2016 22:28:19 +0100 |
traytel |
make predicator a first-class bnf citizen
|
file |
diff |
annotate
|
| Tue, 12 Jan 2016 14:14:28 +0100 |
Andreas Lochbihler |
add BNF instance for Dlist
|
file |
diff |
annotate
|
| Fri, 04 Sep 2015 19:22:13 +0200 |
wenzelm |
modernized name space management -- more uniform qualification;
|
file |
diff |
annotate
|
| Mon, 06 Jul 2015 22:57:34 +0200 |
wenzelm |
tuned proofs;
|
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, 05 Mar 2014 09:59:48 +0100 |
wenzelm |
proper UTF-8;
|
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, 12 Oct 2012 18:58:20 +0200 |
wenzelm |
discontinued obsolete typedef (open) syntax;
|
file |
diff |
annotate
|
| Tue, 17 Jul 2012 23:11:24 +0200 |
haftmann |
tuned whitespace
|
file |
diff |
annotate
|
| Tue, 21 Feb 2012 12:20:33 +0100 |
bulwahn |
subtype preprocessing in Quickcheck;
|
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
|
| Tue, 20 Dec 2011 17:40:17 +0100 |
bulwahn |
adding quickcheck generator for distinct lists; adding examples
|
file |
diff |
annotate
|
| Wed, 30 Nov 2011 16:27:10 +0100 |
wenzelm |
prefer typedef without extra definition and alternative name;
|
file |
diff |
annotate
|
| Mon, 11 Jul 2011 18:44:58 +0200 |
haftmann |
explicit code equation for equality
|
file |
diff |
annotate
|
| Thu, 02 Jun 2011 08:55:08 +0200 |
bulwahn |
splitting Dlist theory in Dlist and Dlist_Cset
|
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
|
| Mon, 22 Nov 2010 17:46:51 +0100 |
haftmann |
replaced misleading Fset/fset name -- these do not stand for finite sets
|
file |
diff |
annotate
|
| Thu, 18 Nov 2010 17:01:15 +0100 |
haftmann |
mapper for dlist type
|
file |
diff |
annotate
|
| Mon, 25 Oct 2010 13:34:58 +0200 |
haftmann |
dropped (almost) redundant distinct.induct rule; distinct_simps again named distinct.simps
|
file |
diff |
annotate
|
| Mon, 04 Oct 2010 12:22:58 +0200 |
haftmann |
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
|
file |
diff |
annotate
|
| Mon, 27 Sep 2010 14:13:22 +0200 |
haftmann |
lemma remdups_list_of_dlist
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 16:43:23 +0200 |
haftmann |
established emerging canonical names *_eqI and *_eq_iff
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 19:34:23 +0200 |
haftmann |
renamed class/constant eq to equal; tuned some instantiations
|
file |
diff |
annotate
|
| Wed, 18 Aug 2010 11:55:27 +0200 |
haftmann |
added equality instantiation
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 08:58:13 +0200 |
haftmann |
dropped superfluous [code del]s
|
file |
diff |
annotate
|
| Mon, 28 Jun 2010 15:32:06 +0200 |
haftmann |
dropped ancient infix mem; refined code generation operations in List.thy
|
file |
diff |
annotate
|
| Mon, 21 Jun 2010 09:06:14 +0200 |
haftmann |
extensionality rule fset_eqI
|
file |
diff |
annotate
|
| Mon, 24 May 2010 13:48:56 +0200 |
haftmann |
induction and case rules
|
file |
diff |
annotate
|
| Thu, 20 May 2010 18:00:48 +0200 |
haftmann |
proper code generator for complement
|
file |
diff |
annotate
|
| Thu, 20 May 2010 16:35:53 +0200 |
haftmann |
moved generic List operations to theory More_List
|
file |
diff |
annotate
|
| Wed, 19 May 2010 09:20:36 +0200 |
haftmann |
added implementations of Fset.Set, Fset.Coset; do not delete code equations for relational operators on fsets
|
file |
diff |
annotate
|
| Thu, 22 Apr 2010 09:30:36 +0200 |
haftmann |
lemma dlist_ext
|
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
|
| Sun, 11 Apr 2010 16:51:07 +0200 |
haftmann |
user interface for abstract datatypes is an attribute, not a command
|
file |
diff |
annotate
|
| Wed, 10 Mar 2010 15:29:22 +0100 |
haftmann |
avoid confusion
|
file |
diff |
annotate
|
| Mon, 22 Feb 2010 15:53:18 +0100 |
haftmann |
added Dlist
|
file |
diff |
annotate
|