Quot/Nominal/Perm.thy
Thu, 25 Feb 2010 07:05:52 +0100 Cezary Kaliszyk Export perm_frees.
Wed, 24 Feb 2010 23:25:30 +0100 Cezary Kaliszyk Restructuring the code in Perm
Wed, 24 Feb 2010 17:42:37 +0100 Cezary Kaliszyk Define lifted perms.
Wed, 24 Feb 2010 15:36:07 +0100 Cezary Kaliszyk Note the instance proofs, since they can be easily lifted.
Wed, 24 Feb 2010 15:13:22 +0100 Cezary Kaliszyk More refactoring and removed references to the global simpset in Perm.
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.
Thu, 18 Feb 2010 11:28:20 +0100 Cezary Kaliszyk Fix for new Isabelle (primrec)
Wed, 17 Feb 2010 13:54:35 +0100 Cezary Kaliszyk Wrapped the permutation code.
Wed, 17 Feb 2010 09:26:10 +0100 Cezary Kaliszyk Simplifying perm_eq
Tue, 16 Feb 2010 15:12:49 +0100 Cezary Kaliszyk Minor
Tue, 16 Feb 2010 14:57:22 +0100 Cezary Kaliszyk Ported Stefan's permutation code, still needs some localizing.
less more (0) tip