| Thu, 23 Dec 2010 00:46:06 +0000 |
Christian Urban |
moved all strong_exhaust code to nominal_dt_quot; tuned examples
|
file |
diff |
annotate
|
| Wed, 22 Dec 2010 10:32:01 +0000 |
Christian Urban |
corrected premises of strong exhausts theorems
|
file |
diff |
annotate
|
| Wed, 22 Dec 2010 09:13:25 +0000 |
Christian Urban |
properly exported strong exhaust theorem; cleaned up some examples
|
file |
diff |
annotate
|
| Sat, 27 Nov 2010 22:55:29 +0000 |
Christian Urban |
disabled the Foo examples, because of heavy work
|
file |
diff |
annotate
|
| Wed, 24 Nov 2010 02:36:21 +0000 |
Christian Urban |
added example from the F-ing paper by Rossberg, Russo and Dreyer
|
file |
diff |
annotate
|
| Mon, 15 Nov 2010 08:17:11 +0000 |
Christian Urban |
added a test for the various shallow binders
|
file |
diff |
annotate
|
| Sun, 14 Nov 2010 16:34:47 +0000 |
Christian Urban |
merged Nominal-General directory into Nominal; renamed Abs.thy to Nominal2_Abs.thy
|
file |
diff |
annotate
|
| Sat, 06 Nov 2010 06:18:41 +0000 |
Christian Urban |
added a test about subtyping; disabled two tests, because of problem with function package
|
file |
diff |
annotate
|
| Tue, 28 Sep 2010 05:56:11 -0400 |
Christian Urban |
added Foo1 to explore a contrived example
|
file |
diff |
annotate
|
| Wed, 22 Sep 2010 18:13:26 +0200 |
Christian Urban |
fixed
|
file |
diff |
annotate
|
| Wed, 22 Sep 2010 14:19:48 +0800 |
Christian Urban |
made supp proofs more robust by not using the standard induction; renamed some example files
|
file |
diff |
annotate
|
| Sun, 29 Aug 2010 13:36:03 +0800 |
Christian Urban |
renamed NewParser to Nominal2
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 03:37:17 +0800 |
Christian Urban |
"isabelle make test" makes all major examples....they work up to supp theorems (excluding)
|
file |
diff |
annotate
|
| Wed, 23 Jun 2010 15:40:00 +0100 |
Christian Urban |
merged cezary's changes
|
file |
diff |
annotate
|
| Thu, 20 May 2010 21:23:53 +0100 |
Christian Urban |
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
|
file |
diff |
annotate
|