Thu, 25 Feb 2010 07:05:52 +0100 |
Cezary Kaliszyk |
Export perm_frees.
|
file |
diff |
annotate
|
Wed, 24 Feb 2010 23:25:30 +0100 |
Cezary Kaliszyk |
Restructuring the code in Perm
|
file |
diff |
annotate
|
Wed, 24 Feb 2010 17:42:37 +0100 |
Cezary Kaliszyk |
Define lifted perms.
|
file |
diff |
annotate
|
Wed, 24 Feb 2010 15:36:07 +0100 |
Cezary Kaliszyk |
Note the instance proofs, since they can be easily lifted.
|
file |
diff |
annotate
|
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
|