| Mon, 19 May 2014 16:45:46 +0100 |
Christian Urban |
changed nominal_primrec to nominal_function and termination to nominal_termination
|
file |
diff |
annotate
|
| Mon, 19 May 2014 12:45:26 +0100 |
Christian Urban |
changed nominal_primrec into the more appropriate nominal_function
|
file |
diff |
annotate
|
| Tue, 07 Aug 2012 18:54:52 +0100 |
Christian Urban |
definition of an auxiliary graph in nominal-primrec definitions
|
file |
diff |
annotate
|
| Sun, 15 Jul 2012 13:03:47 +0100 |
Christian Urban |
added a simproc for alpha-equivalence to the simplifier
|
file |
diff |
annotate
|
| Mon, 04 Jun 2012 21:39:51 +0100 |
Christian Urban |
added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often
|
file |
diff |
annotate
|
| Tue, 19 Jul 2011 02:30:05 +0100 |
Christian Urban |
preliminary version of automatically generation the eqvt-lemmas for functions defined with nominal_primrec
|
file |
diff |
annotate
|
| Tue, 19 Jul 2011 01:40:36 +0100 |
Christian Urban |
generated the partial eqvt-theorem for functions
|
file |
diff |
annotate
|
| Mon, 18 Jul 2011 17:40:13 +0100 |
Christian Urban |
added a flag (eqvt) to termination proofs arising fron nominal_primrecs
|
file |
diff |
annotate
|
| Mon, 18 Jul 2011 00:21:51 +0100 |
Christian Urban |
some tuning
|
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
|
| Mon, 20 Jun 2011 20:09:30 +0900 |
Cezary Kaliszyk |
function for let-rec
|
file |
diff |
annotate
|
| Sun, 29 Aug 2010 13:36:03 +0800 |
Christian Urban |
renamed NewParser to Nominal2
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 02:03:52 +0800 |
Christian Urban |
corrected bug with fv-function generation (that was the problem with recursive binders)
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 02:08:00 +0800 |
Christian Urban |
cleaned up (almost completely) the examples
|
file |
diff |
annotate
| base
|