| Tue, 31 Jul 2012 13:55:39 +0200 |
kuncar |
use lifting/transfer formalization of RBT from Lift_RBT
|
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, 04 May 2012 11:08:31 +0200 |
bulwahn |
using the new transfer method to obtain abstract properties of RBT trees
|
file |
diff |
annotate
|
| Fri, 13 Apr 2012 12:49:33 +0200 |
Andreas Lochbihler |
adapt to changes in RBT_Impl
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 16:26:48 +0200 |
kuncar |
new package Lifting - initial commit
|
file |
diff |
annotate
|
| Fri, 23 Mar 2012 14:26:09 +0100 |
kuncar |
fix example files
|
file |
diff |
annotate
|
| Fri, 23 Mar 2012 14:18:43 +0100 |
kuncar |
store the quotient theorem for every quotient
|
file |
diff |
annotate
|
| Fri, 23 Mar 2012 14:17:29 +0100 |
kuncar |
fix Quotient_Examples
|
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
|
| Fri, 25 Nov 2011 10:52:30 +0100 |
bulwahn |
improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
|
file |
diff |
annotate
|
| Fri, 18 Nov 2011 13:50:01 +0100 |
bulwahn |
adding another example for lifting definitions
|
file |
diff |
annotate
|