| 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
|
| Fri, 30 Aug 2013 14:35:37 +0100 |
Christian Urban |
updated to lates Isabelle
|
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
|
| 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, 16 Jan 2012 13:53:35 +0000 |
Christian Urban |
commented out parts of TypeScheme1 in order to run all tests
|
file |
diff |
annotate
|
| Tue, 03 Jan 2012 11:43:27 +0000 |
Christian Urban |
updated to explicit set type constructor (post Isabelle 3rd January)
|
file |
diff |
annotate
|
| Tue, 03 Jan 2012 01:42:10 +0000 |
Christian Urban |
proved that generalisation is closed under substitution
|
file |
diff |
annotate
|
| Mon, 02 Jan 2012 16:13:16 +0000 |
Christian Urban |
added definition for generalisation of type schemes (for paper)
|
file |
diff |
annotate
|
| Thu, 29 Dec 2011 15:56:54 +0000 |
Christian Urban |
separated the two versions of type schemes into two files
|
file |
diff |
annotate
| base
|