| Fri, 21 Sep 2012 11:51:07 +0200 |
traytel |
tuned antiquotations
|
file |
diff |
annotate
|
| Fri, 21 Sep 2012 11:44:55 +0200 |
traytel |
use iffD* instead of (s)subst instantiated with identity; tuned antiquotations;
|
file |
diff |
annotate
|
| Thu, 20 Sep 2012 17:35:49 +0200 |
blanchet |
finished "disc_coiter_iff" etc. generation
|
file |
diff |
annotate
|
| Thu, 20 Sep 2012 02:42:49 +0200 |
blanchet |
provide predicator, define relator
|
file |
diff |
annotate
|
| Tue, 18 Sep 2012 09:15:53 +0200 |
traytel |
separated registration of BNFs from bnf_def (BNFs are now stored only for bnf_def and (co)data commands)
|
file |
diff |
annotate
|
| Mon, 17 Sep 2012 16:57:22 +0200 |
traytel |
cleaned up internal naming scheme for bnfs
|
file |
diff |
annotate
|
| Sun, 16 Sep 2012 10:33:25 +0200 |
traytel |
use strip_typeN in bnf_def (instead of repairing strip_type)
|
file |
diff |
annotate
|
| Fri, 14 Sep 2012 12:09:27 +0200 |
blanchet |
renamed "mk_UnN" to "mk_UnIN"
|
file |
diff |
annotate
|
| Wed, 12 Sep 2012 23:06:39 +0200 |
blanchet |
rough and ready induction
|
file |
diff |
annotate
|
| Wed, 12 Sep 2012 17:26:05 +0200 |
blanchet |
set up things for (co)induction sugar
|
file |
diff |
annotate
|
| Tue, 11 Sep 2012 22:31:43 +0200 |
blanchet |
support for sort constraints in new (co)data commands
|
file |
diff |
annotate
|
| Tue, 11 Sep 2012 17:09:39 +0200 |
blanchet |
renamed "BNF_Library" to "BNF_Util"
|
file |
diff |
annotate
|
| Mon, 10 Sep 2012 17:35:53 +0200 |
blanchet |
use balanced sums for constructors (to gracefully handle 100 constructors or more)
|
file |
diff |
annotate
|
| Sun, 09 Sep 2012 10:58:11 +0200 |
traytel |
open typedefs everywhere in the package
|
file |
diff |
annotate
|
| Sat, 08 Sep 2012 21:04:26 +0200 |
blanchet |
more sugar on codatatypes
|
file |
diff |
annotate
|
| Sat, 08 Sep 2012 21:04:26 +0200 |
blanchet |
define coiterators
|
file |
diff |
annotate
|
| Sat, 08 Sep 2012 21:04:26 +0200 |
blanchet |
correctly curry recursor arguments
|
file |
diff |
annotate
|
| Thu, 06 Sep 2012 11:46:08 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Thu, 06 Sep 2012 11:34:05 +0200 |
blanchet |
introduced and used "mk_Freesss", and simplified "mk_Freess(')"
|
file |
diff |
annotate
|
| Thu, 06 Sep 2012 02:56:21 +0200 |
blanchet |
construct high-level iterator RHS
|
file |
diff |
annotate
|
| Tue, 04 Sep 2012 13:06:41 +0200 |
blanchet |
more work on sugar + simplify Trueprop + eq idiom everywhere
|
file |
diff |
annotate
|
| Tue, 04 Sep 2012 13:02:32 +0200 |
blanchet |
more work on FP sugar
|
file |
diff |
annotate
|
| Mon, 03 Sep 2012 11:54:21 +0200 |
blanchet |
rearrange dependencies
|
file |
diff |
annotate
|
| Tue, 28 Aug 2012 17:16:00 +0200 |
blanchet |
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
|
file |
diff |
annotate
|