Fri, 30 Apr 2010 15:36:02 +0100 generalised the fs-instance lemma (not just fsets of atoms are finitely supported, but also fsets of finitely supported elements)
Christian Urban <urbanc@in.tum.de> [Fri, 30 Apr 2010 15:36:02 +0100] rev 2004
generalised the fs-instance lemma (not just fsets of atoms are finitely supported, but also fsets of finitely supported elements)
Fri, 30 Apr 2010 15:34:26 +0100 added lemmas establishing the support of finite sets of finitely supported elements
Christian Urban <urbanc@in.tum.de> [Fri, 30 Apr 2010 15:34:26 +0100] rev 2003
added lemmas establishing the support of finite sets of finitely supported elements
Fri, 30 Apr 2010 14:21:18 +0100 added eqvt-lemmas for Bex, Ball and Union
Christian Urban <urbanc@in.tum.de> [Fri, 30 Apr 2010 14:21:18 +0100] rev 2002
added eqvt-lemmas for Bex, Ball and Union
Fri, 30 Apr 2010 15:45:39 +0200 NewParser with Parser functionality, but some cheats included since the order of datayupes is wrong.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 30 Apr 2010 15:45:39 +0200] rev 2001
NewParser with Parser functionality, but some cheats included since the order of datayupes is wrong.
Fri, 30 Apr 2010 14:48:13 +0200 Merged nominal_datatype into NewParser until eqvts
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 30 Apr 2010 14:48:13 +0200] rev 2000
Merged nominal_datatype into NewParser until eqvts
Fri, 30 Apr 2010 13:57:59 +0200 more parser/new parser synchronization.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 30 Apr 2010 13:57:59 +0200] rev 1999
more parser/new parser synchronization.
Fri, 30 Apr 2010 10:48:48 +0200 Simplify old parser for integration
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 30 Apr 2010 10:48:48 +0200] rev 1998
Simplify old parser for integration
Fri, 30 Apr 2010 10:32:34 +0200 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 30 Apr 2010 10:32:34 +0200] rev 1997
merge
Fri, 30 Apr 2010 10:31:32 +0200 Change signature of fv and alpha generation.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 30 Apr 2010 10:31:32 +0200] rev 1996
Change signature of fv and alpha generation.
Fri, 30 Apr 2010 10:09:45 +0100 reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de> [Fri, 30 Apr 2010 10:09:45 +0100] rev 1995
reorganised eqvt-file (now uses perm_simp already)
Fri, 30 Apr 2010 10:04:24 +0200 qpaper
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 30 Apr 2010 10:04:24 +0200] rev 1994
qpaper
Thu, 29 Apr 2010 17:52:33 +0200 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 29 Apr 2010 17:52:33 +0200] rev 1993
merge
Thu, 29 Apr 2010 17:52:19 +0200 New Alpha.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 29 Apr 2010 17:52:19 +0200] rev 1992
New Alpha.
Thu, 29 Apr 2010 17:16:35 +0200 Minimal cleaning in LamEx
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 29 Apr 2010 17:16:35 +0200] rev 1991
Minimal cleaning in LamEx
Thu, 29 Apr 2010 17:03:59 +0200 Remove things moved to the isabelle distribution
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 29 Apr 2010 17:03:59 +0200] rev 1990
Remove things moved to the isabelle distribution
Thu, 29 Apr 2010 16:59:33 +0200 Unify and give only one name to 'setify', 'listify' and 'set'
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 29 Apr 2010 16:59:33 +0200] rev 1989
Unify and give only one name to 'setify', 'listify' and 'set'
Thu, 29 Apr 2010 16:18:38 +0200 Fixing the definitions in the Parser.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 29 Apr 2010 16:18:38 +0200] rev 1988
Fixing the definitions in the Parser.
Thu, 29 Apr 2010 16:16:45 +0200 Some of the exceptions that the parser should check in TODO.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 29 Apr 2010 16:16:45 +0200] rev 1987
Some of the exceptions that the parser should check in TODO.
Thu, 29 Apr 2010 16:15:49 +0200 Extracting the fv body function and exporting the terms.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 29 Apr 2010 16:15:49 +0200] rev 1986
Extracting the fv body function and exporting the terms.
Thu, 29 Apr 2010 13:19:12 +0200 Fix for recursive binders.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 29 Apr 2010 13:19:12 +0200] rev 1985
Fix for recursive binders.
Thu, 29 Apr 2010 12:11:44 +0200 revert 0c9ef14e9ba4
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 29 Apr 2010 12:11:44 +0200] rev 1984
revert 0c9ef14e9ba4
Thu, 29 Apr 2010 11:54:39 +0200 Support in positive position and atoms in negative positions.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 29 Apr 2010 11:54:39 +0200] rev 1983
Support in positive position and atoms in negative positions.
Thu, 29 Apr 2010 11:00:18 +0200 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 29 Apr 2010 11:00:18 +0200] rev 1982
merge
Thu, 29 Apr 2010 10:59:08 +0200 Include support of unknown datatypes in new fv
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 29 Apr 2010 10:59:08 +0200] rev 1981
Include support of unknown datatypes in new fv
Thu, 29 Apr 2010 10:16:33 +0200 merged
Christian Urban <urbanc@in.tum.de> [Thu, 29 Apr 2010 10:16:33 +0200] rev 1980
merged
Thu, 29 Apr 2010 10:16:15 +0200 added basic functions for constructing supp-terms
Christian Urban <urbanc@in.tum.de> [Thu, 29 Apr 2010 10:16:15 +0200] rev 1979
added basic functions for constructing supp-terms
Thu, 29 Apr 2010 10:11:48 +0200 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 29 Apr 2010 10:11:48 +0200] rev 1978
quotient paper
Thu, 29 Apr 2010 09:25:32 +0200 added missing latex-style file
Christian Urban <urbanc@in.tum.de> [Thu, 29 Apr 2010 09:25:32 +0200] rev 1977
added missing latex-style file
Thu, 29 Apr 2010 09:14:16 +0200 merged
Christian Urban <urbanc@in.tum.de> [Thu, 29 Apr 2010 09:14:16 +0200] rev 1976
merged
Thu, 29 Apr 2010 09:13:18 +0200 added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de> [Thu, 29 Apr 2010 09:13:18 +0200] rev 1975
added stub for quotient paper; call with isabelle make qpaper
(0) -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 tip