| Wed, 24 Feb 2010 15:13:22 +0100 | Cezary Kaliszyk | More refactoring and removed references to the global simpset in Perm. | file | diff | annotate |
| Wed, 24 Feb 2010 14:55:09 +0100 | Cezary Kaliszyk | Factor-out 'prove_perm_empty'; I plan to use it in defining permutations on the lifted type. | file | diff | annotate |
| Thu, 18 Feb 2010 11:28:20 +0100 | Cezary Kaliszyk | Fix for new Isabelle (primrec) | file | diff | annotate |
| Wed, 17 Feb 2010 13:54:35 +0100 | Cezary Kaliszyk | Wrapped the permutation code. | file | diff | annotate |
| Wed, 17 Feb 2010 09:26:10 +0100 | Cezary Kaliszyk | Simplifying perm_eq | file | diff | annotate |
| Tue, 16 Feb 2010 15:12:49 +0100 | Cezary Kaliszyk | Minor | file | diff | annotate |
| Tue, 16 Feb 2010 14:57:22 +0100 | Cezary Kaliszyk | Ported Stefan's permutation code, still needs some localizing. | file | diff | annotate |