| Wed, 22 Sep 2010 18:21:48 +0200 |
wenzelm |
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
|
file |
diff |
annotate
|
| Fri, 20 Nov 2009 00:54:20 +0100 |
Christian Urban |
removed fixme - quick-and-dirty flag is appropriate
|
file |
diff |
annotate
|
| Wed, 11 Nov 2009 14:15:11 +0100 |
wenzelm |
uniform use of simultabeous use_thys;
|
file |
diff |
annotate
|
| Mon, 21 Sep 2009 16:01:30 +0200 |
haftmann |
added session theory for Nominal_Examples
|
file |
diff |
annotate
|
| Tue, 21 Oct 2008 21:20:46 +0200 |
berghofe |
Added theory W.
|
file |
diff |
annotate
|
| Sun, 28 Sep 2008 14:40:43 +0200 |
wenzelm |
setmp_noncritical;
|
file |
diff |
annotate
|
| Wed, 16 Jul 2008 17:36:44 +0200 |
berghofe |
Added Standardization theory.
|
file |
diff |
annotate
|
| Thu, 20 Dec 2007 01:07:21 +0100 |
urbanc |
polishing of some proofs
|
file |
diff |
annotate
|
| 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
|