Mon, 18 Jul 2011 17:40:13 +0100 |
Christian Urban |
added a flag (eqvt) to termination proofs arising fron nominal_primrecs
|
file |
diff |
annotate
|
Wed, 13 Jul 2011 09:47:58 +0100 |
Christian Urban |
slight tuning
|
file |
diff |
annotate
|
Mon, 11 Jul 2011 14:02:13 +0200 |
Christian Urban |
combinators for local theories and lists
|
file |
diff |
annotate
|
Fri, 08 Jul 2011 05:04:23 +0200 |
Christian Urban |
some code refactoring
|
file |
diff |
annotate
|
Thu, 07 Jul 2011 16:16:42 +0200 |
Christian Urban |
code refactoring; introduced a record for raw_dt_info
|
file |
diff |
annotate
|
Tue, 05 Jul 2011 18:42:34 +0200 |
Christian Urban |
changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
|
file |
diff |
annotate
|
Tue, 05 Jul 2011 04:18:45 +0200 |
Christian Urban |
exported various FCB-lemmas to a separate file
|
file |
diff |
annotate
|
Thu, 30 Jun 2011 02:19:59 +0100 |
Christian Urban |
more code refactoring
|
file |
diff |
annotate
|
Wed, 29 Jun 2011 23:08:44 +0100 |
Christian Urban |
combined distributed data for alpha in alpha_result (partially done)
|
file |
diff |
annotate
|
Wed, 29 Jun 2011 00:48:50 +0100 |
Christian Urban |
some experiments
|
file |
diff |
annotate
|
Thu, 23 Jun 2011 11:30:39 +0100 |
Christian Urban |
fixed nasty bug with type variables in nominal_datatypes; this included to be careful with the output of the inductive and function package
|
file |
diff |
annotate
|
Wed, 22 Jun 2011 14:14:54 +0100 |
Christian Urban |
tuned
|
file |
diff |
annotate
|
Wed, 22 Jun 2011 13:40:25 +0100 |
Christian Urban |
deleted some dead code
|
file |
diff |
annotate
|
Wed, 22 Jun 2011 12:18:22 +0100 |
Christian Urban |
some rudimentary infrastructure for storing data about nominal datatypes
|
file |
diff |
annotate
|
Thu, 16 Jun 2011 20:07:03 +0100 |
Christian Urban |
got rid of the boolean flag in the raw_equivariance function
|
file |
diff |
annotate
|