| Mon, 19 Apr 2010 09:25:55 +0200 | Cezary Kaliszyk | merge | changeset | files |
| Mon, 19 Apr 2010 09:25:43 +0200 | Cezary Kaliszyk | minor FSet3 edits. | changeset | files |
| Sun, 18 Apr 2010 18:01:22 +0200 | Christian Urban | tuned | changeset | files |
| Sun, 18 Apr 2010 17:58:45 +0200 | Christian Urban | moved some general function into nominal_library.ML | changeset | files |
| Sun, 18 Apr 2010 17:57:27 +0200 | Christian Urban | tuned; transformation functions now take a context, a thm and return a thm | changeset | files |
| Sun, 18 Apr 2010 17:56:05 +0200 | Christian Urban | tuned | changeset | files |
| Sun, 18 Apr 2010 10:58:29 +0200 | Christian Urban | equivariance for alpha_raw in CoreHaskell is automatically derived | changeset | files |
| Sun, 18 Apr 2010 09:26:38 +0200 | Christian Urban | preliminary parser for perm_simp metod | changeset | files |
| Fri, 16 Apr 2010 16:29:11 +0200 | Christian Urban | automatic proofs for equivariance of alphas | changeset | files |
| Fri, 16 Apr 2010 11:09:32 +0200 | Cezary Kaliszyk | Finished proof in Lambda.thy | changeset | files |
| Fri, 16 Apr 2010 10:47:13 +0200 | Christian Urban | merged | changeset | files |
| Fri, 16 Apr 2010 10:46:50 +0200 | Christian Urban | attempt to manual prove eqvt for alpha | changeset | files |
| Fri, 16 Apr 2010 10:41:40 +0200 | Cezary Kaliszyk | Lifting in Term4. | changeset | files |
| Fri, 16 Apr 2010 10:18:16 +0200 | Christian Urban | some tuning of eqvt-infrastructure | changeset | files |
| Thu, 15 Apr 2010 21:56:03 +0200 | Christian Urban | some tuning of proofs | changeset | files |
| Thu, 15 Apr 2010 16:01:28 +0200 | Christian Urban | typo | changeset | files |
| Thu, 15 Apr 2010 15:56:38 +0200 | Christian Urban | merged | changeset | files |
| Thu, 15 Apr 2010 15:56:21 +0200 | Christian Urban | half of the pair-abs-equivalence | changeset | files |
| Thu, 15 Apr 2010 15:31:36 +0200 | Cezary Kaliszyk | More on Manual/Trm4 | changeset | files |
| Thu, 15 Apr 2010 14:08:08 +0200 | Cezary Kaliszyk | alpha4_equivp and constant lifting. | changeset | files |
| Thu, 15 Apr 2010 13:55:44 +0200 | Cezary Kaliszyk | alpha4_eqvt and alpha4_reflp | changeset | files |
| Thu, 15 Apr 2010 12:27:36 +0200 | Cezary Kaliszyk | fv_eqvt in term4 | changeset | files |
| Thu, 15 Apr 2010 12:15:38 +0200 | Cezary Kaliszyk | Updating in Term4. | changeset | files |
| Thu, 15 Apr 2010 12:08:46 +0200 | Cezary Kaliszyk | merge | changeset | files |
| Thu, 15 Apr 2010 11:42:28 +0200 | Cezary Kaliszyk | Prove insert_rsp2 | changeset | files |
| Thu, 15 Apr 2010 12:07:54 +0200 | Christian Urban | merged | changeset | files |
| Thu, 15 Apr 2010 12:07:34 +0200 | Christian Urban | changed header | changeset | files |
| Thu, 15 Apr 2010 11:05:54 +0200 | Cezary Kaliszyk | Minor paper fixes. | changeset | files |
| Wed, 14 Apr 2010 22:41:22 +0200 | Christian Urban | temporary fix for CoreHaskell | changeset | files |
| 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 | changeset | files |
| Wed, 14 Apr 2010 20:21:11 +0200 | Cezary Kaliszyk | merge | changeset | files |
| Wed, 14 Apr 2010 20:20:54 +0200 | Cezary Kaliszyk | Fix the 'subscript' error. | changeset | files |
| Wed, 14 Apr 2010 18:47:20 +0200 | Christian Urban | merged | changeset | files |
| Wed, 14 Apr 2010 18:46:59 +0200 | Christian Urban | thmdecls can deal with lemmas like alpha_gen which contain pairs or tuples | changeset | files |
| Wed, 14 Apr 2010 16:11:04 +0200 | Cezary Kaliszyk | merge | changeset | files |
| Wed, 14 Apr 2010 16:10:44 +0200 | Cezary Kaliszyk | merge | changeset | files |
| Wed, 14 Apr 2010 11:08:33 +0200 | Cezary Kaliszyk | Separate alpha_definition. | changeset | files |
| Wed, 14 Apr 2010 11:07:42 +0200 | Cezary Kaliszyk | Fix spelling in theory header | changeset | files |
| Wed, 14 Apr 2010 10:50:11 +0200 | Cezary Kaliszyk | Separate define_fv. | changeset | files |
| Wed, 14 Apr 2010 16:05:58 +0200 | Christian Urban | tuned and removed dead code | changeset | files |
| Wed, 14 Apr 2010 15:02:07 +0200 | Christian Urban | moved a couple of more functions to the library | changeset | files |
| Wed, 14 Apr 2010 14:41:54 +0200 | Christian Urban | added a library for basic nominal functions; separated nominal_eqvt file | changeset | files |
| Wed, 14 Apr 2010 13:21:38 +0200 | Christian Urban | merged | changeset | files |
| Wed, 14 Apr 2010 13:21:11 +0200 | Christian Urban | first working version of the automatic equivariance procedure | changeset | files |
| Wed, 14 Apr 2010 10:39:03 +0200 | Cezary Kaliszyk | Initial cleaning/reorganization in Fv. | changeset | files |
| Wed, 14 Apr 2010 10:29:56 +0200 | Christian Urban | merged | changeset | files |
| Wed, 14 Apr 2010 10:29:34 +0200 | Christian Urban | preliminary tests | changeset | files |
| Wed, 14 Apr 2010 10:28:17 +0200 | Christian Urban | deleted test | changeset | files |
| Wed, 14 Apr 2010 08:42:38 +0200 | Cezary Kaliszyk | merge | changeset | files |
| Wed, 14 Apr 2010 08:36:54 +0200 | Cezary Kaliszyk | merge part: delete_rsp | changeset | files |
| Wed, 14 Apr 2010 08:35:31 +0200 | Cezary Kaliszyk | merge part1: none_memb_nil | changeset | files |
| Wed, 14 Apr 2010 08:16:54 +0200 | Christian Urban | added header and more tuning | changeset | files |
| Wed, 14 Apr 2010 07:57:55 +0200 | Christian Urban | more tuning | changeset | files |
| Wed, 14 Apr 2010 07:34:03 +0200 | Christian Urban | tuned | changeset | files |
| Tue, 13 Apr 2010 15:59:53 +0200 | Cezary Kaliszyk | Working FSet with additional lemmas. | changeset | files |
| Tue, 13 Apr 2010 15:00:49 +0200 | Cezary Kaliszyk | Much more in FSet (currently non-working) | changeset | files |
| Tue, 13 Apr 2010 07:40:54 +0200 | Christian Urban | made everything to compile | changeset | files |
| Tue, 13 Apr 2010 00:53:48 +0200 | Christian Urban | merged | changeset | files |
| Tue, 13 Apr 2010 00:53:32 +0200 | Christian Urban | some small tunings (incompleted work in Lambda.thy) | changeset | files |
| Tue, 13 Apr 2010 00:47:57 +0200 | Christian Urban | moved equivariance of map into Nominal2_Eqvt file | changeset | files |