| Fri, 26 Mar 2010 22:22:41 +0100 | Cezary Kaliszyk | Modified abs_gen_sym and abs_gen_trans so it becomes usable in the proofs. | file | diff | annotate |
| Fri, 26 Mar 2010 22:02:59 +0100 | Christian Urban | more on the paper | file | diff | annotate |
| Fri, 26 Mar 2010 18:44:47 +0100 | Christian Urban | simplification | file | diff | annotate |
| Fri, 26 Mar 2010 16:46:40 +0100 | Christian Urban | merged | file | diff | annotate |
| Tue, 23 Mar 2010 07:43:20 +0100 | Christian Urban | merged | file | diff | annotate |
| Tue, 23 Mar 2010 07:39:10 +0100 | Christian Urban | more on the paper | file | diff | annotate |
| Tue, 23 Mar 2010 07:04:14 +0100 | Cezary Kaliszyk | Remove compose_eqvt | file | diff | annotate |
| Mon, 22 Mar 2010 18:29:29 +0100 | Cezary Kaliszyk | equivp_cheat can be removed for all one-permutation examples. | file | diff | annotate |
| 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 |
| Mon, 15 Mar 2010 17:51:35 +0100 | Christian Urban | proof for support when bn-function is present, but fb_function is empty | file | diff | annotate |
| Mon, 15 Mar 2010 10:02:19 +0100 | Cezary Kaliszyk | Prove alpha_gen_compose_eqvt | file | diff | annotate |
| Mon, 15 Mar 2010 08:39:23 +0100 | Christian Urban | added preliminary test version....but Test works now | file | diff | annotate |
| Thu, 11 Mar 2010 20:49:31 +0100 | Cezary Kaliszyk | Do not fail if the finite support proof fails. | file | diff | annotate |
| Thu, 11 Mar 2010 19:43:50 +0100 | Christian Urban | generalised the supp for atoms to all concrete atoms (not just names) | file | diff | annotate |