| 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
|
| Mon, 05 Mar 2012 16:27:28 +0000 |
Christian Urban |
updated tutorial to latest version and added it to the tests
|
file |
diff |
annotate
|
| Fri, 04 Feb 2011 03:52:38 +0000 |
Christian Urban |
Lambda.thy which works with Nominal_Isabelle2011
|
file |
diff |
annotate
|
| Sat, 22 Jan 2011 18:59:48 -0600 |
Christian Urban |
cleaning up
|
file |
diff |
annotate
|
| Wed, 19 Jan 2011 23:58:12 +0100 |
Christian Urban |
added a very rough version of the tutorial; all seems to work
|
file |
diff |
annotate
|
| Wed, 19 Jan 2011 19:06:52 +0100 |
Christian Urban |
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
|
file |
diff |
annotate
|