Christian Urban <urbanc@in.tum.de> [Tue, 20 Apr 2010 08:45:53 +0200] rev 1900
added comment about abstraction in raw permuations
Christian Urban <urbanc@in.tum.de> [Tue, 20 Apr 2010 07:44:47 +0200] rev 1899
optimised the code of define_raw_perm
Christian Urban <urbanc@in.tum.de> [Mon, 19 Apr 2010 17:26:07 +0200] rev 1898
deleting function perm_arg in favour of the library function mk_perm
Christian Urban <urbanc@in.tum.de> [Mon, 19 Apr 2010 16:55:57 +0200] rev 1897
merged
Christian Urban <urbanc@in.tum.de> [Mon, 19 Apr 2010 16:55:36 +0200] rev 1896
tuned; fleshed out some library functions about permutations; closed Datatype_Aux structure (increases readability)
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 19 Apr 2010 16:19:17 +0200] rev 1895
FSet is a semi-lattice
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 19 Apr 2010 15:54:55 +0200] rev 1894
merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 19 Apr 2010 15:54:38 +0200] rev 1893
Putting FSet in bot typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 19 Apr 2010 15:33:19 +0200] rev 1892
reorder
Christian Urban <urbanc@in.tum.de> [Mon, 19 Apr 2010 15:37:54 +0200] rev 1891
merged
Christian Urban <urbanc@in.tum.de> [Mon, 19 Apr 2010 15:37:33 +0200] rev 1890
small updates to the paper; remaining points in PAPER-TODO
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 19 Apr 2010 15:28:57 +0200] rev 1889
sub_list definition and respects
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 19 Apr 2010 15:08:29 +0200] rev 1888
Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 19 Apr 2010 14:08:01 +0200] rev 1887
Some new lemmas
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 19 Apr 2010 13:58:10 +0200] rev 1886
More cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 19 Apr 2010 12:28:48 +0200] rev 1885
remove more metis
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 19 Apr 2010 12:20:18 +0200] rev 1884
more metis cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 19 Apr 2010 11:55:12 +0200] rev 1883
Getting rid of 'metis'.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 19 Apr 2010 11:38:43 +0200] rev 1882
merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 19 Apr 2010 11:32:33 +0200] rev 1881
Remove 'defer'.
Christian Urban <urbanc@in.tum.de> [Mon, 19 Apr 2010 09:27:53 +0200] rev 1880
merged
Christian Urban <urbanc@in.tum.de> [Mon, 19 Apr 2010 09:25:31 +0200] rev 1879
tuned proofs
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 19 Apr 2010 11:04:31 +0200] rev 1878
2 more lifted lemmas needed for second representation
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 19 Apr 2010 10:35:08 +0200] rev 1877
Accept non-equality eqvt rules in support proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 19 Apr 2010 10:00:52 +0200] rev 1876
merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 19 Apr 2010 09:59:32 +0200] rev 1875
Locations of files in Parser
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 19 Apr 2010 09:25:55 +0200] rev 1874
merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 19 Apr 2010 09:25:43 +0200] rev 1873
minor FSet3 edits.
Christian Urban <urbanc@in.tum.de> [Sun, 18 Apr 2010 18:01:22 +0200] rev 1872
tuned
Christian Urban <urbanc@in.tum.de> [Sun, 18 Apr 2010 17:58:45 +0200] rev 1871
moved some general function into nominal_library.ML