Fri, 16 Apr 2010 10:46:50 +0200 Christian Urban attempt to manual prove eqvt for alpha
Fri, 16 Apr 2010 10:41:40 +0200 Cezary Kaliszyk Lifting in Term4.
Fri, 16 Apr 2010 10:18:16 +0200 Christian Urban some tuning of eqvt-infrastructure
Thu, 15 Apr 2010 21:56:03 +0200 Christian Urban some tuning of proofs
Thu, 15 Apr 2010 16:01:28 +0200 Christian Urban typo
Thu, 15 Apr 2010 15:56:38 +0200 Christian Urban merged
Thu, 15 Apr 2010 15:56:21 +0200 Christian Urban half of the pair-abs-equivalence
Thu, 15 Apr 2010 15:31:36 +0200 Cezary Kaliszyk More on Manual/Trm4
Thu, 15 Apr 2010 14:08:08 +0200 Cezary Kaliszyk alpha4_equivp and constant lifting.
Thu, 15 Apr 2010 13:55:44 +0200 Cezary Kaliszyk alpha4_eqvt and alpha4_reflp
Thu, 15 Apr 2010 12:27:36 +0200 Cezary Kaliszyk fv_eqvt in term4
Thu, 15 Apr 2010 12:15:38 +0200 Cezary Kaliszyk Updating in Term4.
Thu, 15 Apr 2010 12:08:46 +0200 Cezary Kaliszyk merge
Thu, 15 Apr 2010 11:42:28 +0200 Cezary Kaliszyk Prove insert_rsp2
Thu, 15 Apr 2010 12:07:54 +0200 Christian Urban merged
Thu, 15 Apr 2010 12:07:34 +0200 Christian Urban changed header
Thu, 15 Apr 2010 11:05:54 +0200 Cezary Kaliszyk Minor paper fixes.
Wed, 14 Apr 2010 22:41:22 +0200 Christian Urban temporary fix for CoreHaskell
Wed, 14 Apr 2010 22:23:52 +0200 Christian Urban deleted offending [eqvt]-attribute in Abs; Lambda works again, but there is now a problem in CoreHaskell
Wed, 14 Apr 2010 20:21:11 +0200 Cezary Kaliszyk merge
Wed, 14 Apr 2010 20:20:54 +0200 Cezary Kaliszyk Fix the 'subscript' error.
Wed, 14 Apr 2010 18:47:20 +0200 Christian Urban merged
Wed, 14 Apr 2010 18:46:59 +0200 Christian Urban thmdecls can deal with lemmas like alpha_gen which contain pairs or tuples
Wed, 14 Apr 2010 16:11:04 +0200 Cezary Kaliszyk merge
Wed, 14 Apr 2010 16:10:44 +0200 Cezary Kaliszyk merge
Wed, 14 Apr 2010 11:08:33 +0200 Cezary Kaliszyk Separate alpha_definition.
Wed, 14 Apr 2010 11:07:42 +0200 Cezary Kaliszyk Fix spelling in theory header
Wed, 14 Apr 2010 10:50:11 +0200 Cezary Kaliszyk Separate define_fv.
Wed, 14 Apr 2010 16:05:58 +0200 Christian Urban tuned and removed dead code
Wed, 14 Apr 2010 15:02:07 +0200 Christian Urban moved a couple of more functions to the library
Wed, 14 Apr 2010 14:41:54 +0200 Christian Urban added a library for basic nominal functions; separated nominal_eqvt file
Wed, 14 Apr 2010 13:21:38 +0200 Christian Urban merged
Wed, 14 Apr 2010 13:21:11 +0200 Christian Urban first working version of the automatic equivariance procedure
Wed, 14 Apr 2010 10:39:03 +0200 Cezary Kaliszyk Initial cleaning/reorganization in Fv.
Wed, 14 Apr 2010 10:29:56 +0200 Christian Urban merged
Wed, 14 Apr 2010 10:29:34 +0200 Christian Urban preliminary tests
Wed, 14 Apr 2010 10:28:17 +0200 Christian Urban deleted test
Wed, 14 Apr 2010 08:42:38 +0200 Cezary Kaliszyk merge
Wed, 14 Apr 2010 08:36:54 +0200 Cezary Kaliszyk merge part: delete_rsp
Wed, 14 Apr 2010 08:35:31 +0200 Cezary Kaliszyk merge part1: none_memb_nil
Wed, 14 Apr 2010 08:16:54 +0200 Christian Urban added header and more tuning
Wed, 14 Apr 2010 07:57:55 +0200 Christian Urban more tuning
Wed, 14 Apr 2010 07:34:03 +0200 Christian Urban tuned
Tue, 13 Apr 2010 15:59:53 +0200 Cezary Kaliszyk Working FSet with additional lemmas.
Tue, 13 Apr 2010 15:00:49 +0200 Cezary Kaliszyk Much more in FSet (currently non-working)
Tue, 13 Apr 2010 07:40:54 +0200 Christian Urban made everything to compile
Tue, 13 Apr 2010 00:53:48 +0200 Christian Urban merged
Tue, 13 Apr 2010 00:53:32 +0200 Christian Urban some small tunings (incompleted work in Lambda.thy)
Tue, 13 Apr 2010 00:47:57 +0200 Christian Urban moved equivariance of map into Nominal2_Eqvt file
Mon, 12 Apr 2010 17:44:26 +0200 Christian Urban early ott paper
Mon, 12 Apr 2010 17:05:19 +0200 Cezary Kaliszyk Porting lemmas from Quotient package FSet to new FSet.
Mon, 12 Apr 2010 14:31:23 +0200 Christian Urban added alpha-caml paper
Mon, 12 Apr 2010 13:34:54 +0200 Christian Urban implemented in thmdecls the case where eqvt-lemmas are of the form _ ==> _
Sun, 11 Apr 2010 22:48:49 +0200 Christian Urban fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _
Sun, 11 Apr 2010 22:47:45 +0200 Christian Urban folded changes from the conference version
Sun, 11 Apr 2010 22:01:56 +0200 Christian Urban added TODO item about parser creating syntax for the wrong type
Sun, 11 Apr 2010 18:18:22 +0200 Christian Urban corrected imports header
Sun, 11 Apr 2010 18:11:23 +0200 Christian Urban tuned
Sun, 11 Apr 2010 18:11:13 +0200 Christian Urban a few tests
Sun, 11 Apr 2010 18:10:08 +0200 Christian Urban added eqvt rules that are more standard
(0) -1000 -300 -100 -60 +60 +100 +300 +1000 tip