Sat, 13 Dec 2008 13:24:45 +0100 |
berghofe |
Modified nominal_primrec to make it work with local theories, unified syntax
|
file |
diff |
annotate
|
Thu, 12 Jun 2008 09:41:13 +0200 |
urbanc |
emoved the parts that deal with the CK machine to a new theory
|
file |
diff |
annotate
|
Thu, 22 May 2008 16:34:41 +0200 |
urbanc |
made the naming of the induction principles consistent: weak_induct is
|
file |
diff |
annotate
|
Fri, 16 May 2008 22:35:25 +0200 |
urbanc |
added a lemma about existence of contexts
|
file |
diff |
annotate
|
Fri, 02 May 2008 02:16:10 +0200 |
urbanc |
tuned some proofs and comments
|
file |
diff |
annotate
|
Tue, 08 Jan 2008 23:11:08 +0100 |
urbanc |
tuned proofs
|
file |
diff |
annotate
|
Mon, 07 Jan 2008 02:24:24 +0100 |
urbanc |
some pre-release tunings
|
file |
diff |
annotate
|
Tue, 01 Jan 2008 07:28:20 +0100 |
urbanc |
tuned proofs and comments
|
file |
diff |
annotate
|
Thu, 20 Dec 2007 01:07:21 +0100 |
urbanc |
polishing of some proofs
|
file |
diff |
annotate
|
Wed, 28 Nov 2007 18:39:53 +0100 |
urbanc |
an example file for how to treat Felleisen-Hieb-style contexts
|
file |
diff |
annotate
|