| Sat, 20 Mar 2010 13:50:00 +0100 |
Christian Urban |
moved lemmas supp_perm_eq and exists_perm to Nominal2_Supp
|
file |
diff |
annotate
|
| Sat, 20 Mar 2010 04:51:26 +0100 |
Christian Urban |
started cleaning up and introduced 3 versions of ~~gen
|
file |
diff |
annotate
|
| Sat, 20 Mar 2010 02:46:07 +0100 |
Christian Urban |
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
|
file |
diff |
annotate
|
| Fri, 19 Mar 2010 12:28:35 +0100 |
Cezary Kaliszyk |
Keep only one copy of infinite_Un.
|
file |
diff |
annotate
|
| Fri, 19 Mar 2010 12:24:16 +0100 |
Cezary Kaliszyk |
Added a missing 'import'.
|
file |
diff |
annotate
|
| Fri, 19 Mar 2010 12:22:10 +0100 |
Cezary Kaliszyk |
Showed the instance: fset::(at) fs
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 17:40:14 +0100 |
Cezary Kaliszyk |
Proper compose_sym2
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 17:09:01 +0100 |
Cezary Kaliszyk |
Trying to find a compose lemma for 2 arguments.
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 11:53:56 +0100 |
Christian Urban |
added proof of supp/fv for type schemes
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 09:25:01 +0100 |
Cezary Kaliszyk |
Fix for the change of alpha_gen.
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 09:18:27 +0100 |
Cezary Kaliszyk |
merge
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 08:39:46 +0100 |
Cezary Kaliszyk |
Lifting theorems with compound fv and compound alpha.
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 06:49:33 +0100 |
Christian Urban |
added another supp-proof for the non-recursive case
|
file |
diff |
annotate
|
| Tue, 16 Mar 2010 18:02:08 +0100 |
Christian Urban |
merge and proof of support for non-recursive case
|
file |
diff |
annotate
|
| Mon, 15 Mar 2010 23:42:56 +0100 |
Christian Urban |
merged (confirmed to work with Isabelle from 6th March)
|
file |
diff |
annotate
|