Wed, 21 Apr 2010 10:09:07 +0200 merged
Christian Urban <urbanc@in.tum.de> [Wed, 21 Apr 2010 10:09:07 +0200] rev 1913
merged
Wed, 21 Apr 2010 10:08:47 +0200 removed a sorry
Christian Urban <urbanc@in.tum.de> [Wed, 21 Apr 2010 10:08:47 +0200] rev 1912
removed a sorry
Tue, 20 Apr 2010 18:24:50 +0200 renamed Ex1.thy to SingleLet.thy
Christian Urban <urbanc@in.tum.de> [Tue, 20 Apr 2010 18:24:50 +0200] rev 1911
renamed Ex1.thy to SingleLet.thy
Tue, 20 Apr 2010 11:29:00 +0200 tuning of the code
Christian Urban <urbanc@in.tum.de> [Tue, 20 Apr 2010 11:29:00 +0200] rev 1910
tuning of the code
Wed, 21 Apr 2010 09:48:35 +0200 Reorder FSet
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 21 Apr 2010 09:48:35 +0200] rev 1909
Reorder FSet
Wed, 21 Apr 2010 09:13:55 +0200 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 21 Apr 2010 09:13:55 +0200] rev 1908
merge
Wed, 21 Apr 2010 09:13:32 +0200 lattice properties.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 21 Apr 2010 09:13:32 +0200] rev 1907
lattice properties.
Tue, 20 Apr 2010 17:25:31 +0200 All lifted in Term4. Requires new isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 20 Apr 2010 17:25:31 +0200] rev 1906
All lifted in Term4. Requires new isabelle.
Tue, 20 Apr 2010 15:59:57 +0200 fsets are distributive lattices.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 20 Apr 2010 15:59:57 +0200] rev 1905
fsets are distributive lattices.
Tue, 20 Apr 2010 10:23:39 +0200 Fix of comment
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 20 Apr 2010 10:23:39 +0200] rev 1904
Fix of comment
Tue, 20 Apr 2010 09:13:52 +0200 reordered code
Christian Urban <urbanc@in.tum.de> [Tue, 20 Apr 2010 09:13:52 +0200] rev 1903
reordered code
Tue, 20 Apr 2010 09:02:22 +0200 renamed "_empty" and "_append" to "_zero" and "_plus"
Christian Urban <urbanc@in.tum.de> [Tue, 20 Apr 2010 09:02:22 +0200] rev 1902
renamed "_empty" and "_append" to "_zero" and "_plus"
Tue, 20 Apr 2010 08:57:13 +0200 removed dead code (nominal cannot deal with argument types of constructors that are functions)
Christian Urban <urbanc@in.tum.de> [Tue, 20 Apr 2010 08:57:13 +0200] rev 1901
removed dead code (nominal cannot deal with argument types of constructors that are functions)
Tue, 20 Apr 2010 08:45:53 +0200 added comment about abstraction in raw permuations
Christian Urban <urbanc@in.tum.de> [Tue, 20 Apr 2010 08:45:53 +0200] rev 1900
added comment about abstraction in raw permuations
Tue, 20 Apr 2010 07:44:47 +0200 optimised the code of define_raw_perm
Christian Urban <urbanc@in.tum.de> [Tue, 20 Apr 2010 07:44:47 +0200] rev 1899
optimised the code of define_raw_perm
Mon, 19 Apr 2010 17:26:07 +0200 deleting function perm_arg in favour of the library function mk_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
Mon, 19 Apr 2010 16:55:57 +0200 merged
Christian Urban <urbanc@in.tum.de> [Mon, 19 Apr 2010 16:55:57 +0200] rev 1897
merged
Mon, 19 Apr 2010 16:55:36 +0200 tuned; fleshed out some library functions about permutations; closed Datatype_Aux structure (increases readability)
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)
Mon, 19 Apr 2010 16:19:17 +0200 FSet is a semi-lattice
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 19 Apr 2010 16:19:17 +0200] rev 1895
FSet is a semi-lattice
Mon, 19 Apr 2010 15:54:55 +0200 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 19 Apr 2010 15:54:55 +0200] rev 1894
merge
Mon, 19 Apr 2010 15:54:38 +0200 Putting FSet in bot typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 19 Apr 2010 15:54:38 +0200] rev 1893
Putting FSet in bot typeclass.
Mon, 19 Apr 2010 15:33:19 +0200 reorder
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 19 Apr 2010 15:33:19 +0200] rev 1892
reorder
Mon, 19 Apr 2010 15:37:54 +0200 merged
Christian Urban <urbanc@in.tum.de> [Mon, 19 Apr 2010 15:37:54 +0200] rev 1891
merged
Mon, 19 Apr 2010 15:37:33 +0200 small updates to the paper; remaining points in PAPER-TODO
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
Mon, 19 Apr 2010 15:28:57 +0200 sub_list definition and respects
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 19 Apr 2010 15:28:57 +0200] rev 1889
sub_list definition and respects
Mon, 19 Apr 2010 15:08:29 +0200 Alternate list_eq and equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 19 Apr 2010 15:08:29 +0200] rev 1888
Alternate list_eq and equivalence
Mon, 19 Apr 2010 14:08:01 +0200 Some new lemmas
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 19 Apr 2010 14:08:01 +0200] rev 1887
Some new lemmas
Mon, 19 Apr 2010 13:58:10 +0200 More cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 19 Apr 2010 13:58:10 +0200] rev 1886
More cleaning
Mon, 19 Apr 2010 12:28:48 +0200 remove more metis
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 19 Apr 2010 12:28:48 +0200] rev 1885
remove more metis
Mon, 19 Apr 2010 12:20:18 +0200 more metis cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 19 Apr 2010 12:20:18 +0200] rev 1884
more metis cleaning
(0) -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 tip