| Mon, 08 Oct 2007 07:05:54 +0200 |
urbanc |
changed file name
|
file |
diff |
annotate
|
| Mon, 08 Oct 2007 05:23:47 +0200 |
urbanc |
added two new example files
|
file |
diff |
annotate
|
| Fri, 03 Aug 2007 22:50:40 +0200 |
wenzelm |
simultaneous use_thys;
|
file |
diff |
annotate
|
| Wed, 13 Jun 2007 14:21:54 +0200 |
wenzelm |
reactivated theory Class;
|
file |
diff |
annotate
|
| Wed, 06 Jun 2007 21:24:35 +0200 |
urbanc |
take out Class.thy again, because it does not yet compile cleanly
|
file |
diff |
annotate
|
| Tue, 05 Jun 2007 09:56:19 +0200 |
urbanc |
included Class.thy in the compiling process for Nominal/Examples
|
file |
diff |
annotate
|
| Thu, 31 May 2007 14:47:20 +0200 |
urbanc |
introduced symmetric variants of the lemmas for alpha-equivalence
|
file |
diff |
annotate
|
| Thu, 31 May 2007 11:00:06 +0200 |
wenzelm |
fixed use_thy "LocalWeakening";
|
file |
diff |
annotate
|
| Thu, 31 May 2007 10:17:23 +0200 |
urbanc |
included new example in the compiling process
|
file |
diff |
annotate
|
| Fri, 25 May 2007 05:18:56 +0200 |
urbanc |
took out Class.thy from the compiling process until memory problems are solved
|
file |
diff |
annotate
|
| Fri, 27 Apr 2007 18:50:27 +0200 |
urbanc |
tuned some proofs in CR and properly included CR_Takahashi
|
file |
diff |
annotate
|
| Fri, 16 Mar 2007 17:17:36 +0100 |
urbanc |
adjusted for the example file SOS.thy
|
file |
diff |
annotate
|
| Tue, 16 Jan 2007 13:59:08 +0100 |
urbanc |
formalisation of Crary's chapter on logical relations
|
file |
diff |
annotate
|
| Wed, 01 Nov 2006 15:50:19 +0100 |
urbanc |
tuned
|
file |
diff |
annotate
|
| Mon, 23 Oct 2006 00:48:45 +0200 |
berghofe |
Added Compile and Height examples.
|
file |
diff |
annotate
|
| Fri, 28 Apr 2006 17:56:20 +0200 |
berghofe |
Added Class, Fsub, and Lambda_mu examples for nominal datatypes.
|
file |
diff |
annotate
|
| Fri, 28 Apr 2006 15:55:38 +0200 |
berghofe |
New ROOT file for nominal datatype examples.
|
file |
diff |
annotate
|