| Tue, 13 Aug 2013 16:25:47 +0200 |
wenzelm |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
file |
diff |
annotate
|
| 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
|