| Wed, 10 Nov 2010 13:46:21 +0000 |
Christian Urban |
adapted to changes by Florian on the quotient package and removed local fix for function package
|
file |
diff |
annotate
|
| Thu, 28 Oct 2010 14:03:46 +0900 |
Cezary Kaliszyk |
Remove FSet and use the one from Isabelle
|
file |
diff |
annotate
|
| Sun, 17 Oct 2010 15:53:37 +0100 |
Christian Urban |
all tests work again
|
file |
diff |
annotate
|
| Sun, 17 Oct 2010 13:35:52 +0100 |
Christian Urban |
naming scheme is now *_fset (not f*_)
|
file |
diff |
annotate
|
| Fri, 15 Oct 2010 15:56:16 +0100 |
Christian Urban |
slight update
|
file |
diff |
annotate
|
| Thu, 14 Oct 2010 04:14:22 +0100 |
Christian Urban |
major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
|
file |
diff |
annotate
|
| Sat, 04 Sep 2010 07:39:38 +0800 |
Christian Urban |
got rid of Nominal2_Supp (is now in Nomina2_Base)
|
file |
diff |
annotate
|
| Sat, 04 Sep 2010 06:23:31 +0800 |
Christian Urban |
moved a proof to Abs
|
file |
diff |
annotate
|
| Sat, 04 Sep 2010 06:10:04 +0800 |
Christian Urban |
got rid of Nominal_Atoms (folded into Nominal2_Base)
|
file |
diff |
annotate
|
| Sat, 04 Sep 2010 05:43:03 +0800 |
Christian Urban |
cleaned a bit various thy-files in Nominal-General
|
file |
diff |
annotate
|
| Sat, 28 Aug 2010 18:15:23 +0800 |
Christian Urban |
slight cleaning
|
file |
diff |
annotate
|
| Tue, 29 Jun 2010 18:00:59 +0100 |
Christian Urban |
removed an "eqvt"-warning
|
file |
diff |
annotate
|
| Thu, 27 May 2010 18:37:52 +0200 |
Christian Urban |
intermediate state
|
file |
diff |
annotate
|
| Tue, 25 May 2010 17:01:37 +0200 |
Cezary Kaliszyk |
reversing the direction of fresh_star
|
file |
diff |
annotate
|
| Fri, 30 Apr 2010 15:36:02 +0100 |
Christian Urban |
generalised the fs-instance lemma (not just fsets of atoms are finitely supported, but also fsets of finitely supported elements)
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 08:32:33 +0200 |
Christian Urban |
use the more general type-class at_base
|
file |
diff |
annotate
|
| Thu, 22 Apr 2010 05:16:23 +0200 |
Christian Urban |
moved lemmas from FSet.thy to do with atom to Nominal2_Base, and to do with 'a::at set to Nominal2_Atoms; moved Nominal2_Eqvt.thy one up to be loaded before Nominal2_Atoms
|
file |
diff |
annotate
|
| Tue, 13 Apr 2010 07:40:54 +0200 |
Christian Urban |
made everything to compile
|
file |
diff |
annotate
|
| Tue, 13 Apr 2010 00:47:57 +0200 |
Christian Urban |
moved equivariance of map into Nominal2_Eqvt file
|
file |
diff |
annotate
|
| Sun, 11 Apr 2010 18:11:23 +0200 |
Christian Urban |
tuned
|
file |
diff |
annotate
|
| Thu, 08 Apr 2010 00:00:21 -0700 |
Brian Huffman |
simplify instance proof
|
file |
diff |
annotate
|
| Sun, 04 Apr 2010 21:39:28 +0200 |
Christian Urban |
separated general nominal theory into separate folder
|
file |
diff |
annotate
|
| Sat, 27 Mar 2010 14:38:22 +0100 |
Cezary Kaliszyk |
Remove list_eq notation.
|
file |
diff |
annotate
|
| Sat, 27 Mar 2010 09:21:43 +0100 |
Cezary Kaliszyk |
Generalize Abs_eq_iff.
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 10:15:46 +0100 |
Cezary Kaliszyk |
Strong induction for Type Schemes.
|
file |
diff |
annotate
|
| Fri, 19 Mar 2010 12:22:10 +0100 |
Cezary Kaliszyk |
Showed the instance: fset::(at) fs
|
file |
diff |
annotate
|
| Fri, 19 Mar 2010 08:31:43 +0100 |
Cezary Kaliszyk |
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
|
file |
diff |
annotate
|