| Mon, 19 Apr 2010 09:27:53 +0200 | Christian Urban | merged | changeset | files |
| Mon, 19 Apr 2010 09:25:31 +0200 | Christian Urban | tuned proofs | changeset | files |
| Mon, 19 Apr 2010 11:04:31 +0200 | Cezary Kaliszyk | 2 more lifted lemmas needed for second representation | changeset | files |
| Mon, 19 Apr 2010 10:35:08 +0200 | Cezary Kaliszyk | Accept non-equality eqvt rules in support proofs. | changeset | files |
| Mon, 19 Apr 2010 10:00:52 +0200 | Cezary Kaliszyk | merge | changeset | files |
| Mon, 19 Apr 2010 09:59:32 +0200 | Cezary Kaliszyk | Locations of files in Parser | changeset | files |
| 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 |