| Fri, 04 Dec 2009 16:53:11 +0100 | Cezary Kaliszyk | more name cleaning and removing | changeset | files |
| Fri, 04 Dec 2009 16:40:23 +0100 | Cezary Kaliszyk | More code cleaning and renaming: moved rsp and prs lemmas from Int to QuotList | changeset | files |
| Fri, 04 Dec 2009 16:12:40 +0100 | Cezary Kaliszyk | Cleaning & Renaming coming from QuotList | changeset | files |
| Fri, 04 Dec 2009 16:01:23 +0100 | Cezary Kaliszyk | Cleaning in Quotients | changeset | files |
| Fri, 04 Dec 2009 15:50:57 +0100 | Cezary Kaliszyk | Even more name changes and cleaning | changeset | files |
| Fri, 04 Dec 2009 15:41:09 +0100 | Cezary Kaliszyk | More code cleaning and name changes | changeset | files |
| Fri, 04 Dec 2009 15:25:51 +0100 | Cezary Kaliszyk | merge | changeset | files |
| Fri, 04 Dec 2009 15:25:26 +0100 | Cezary Kaliszyk | merged | changeset | files |
| Fri, 04 Dec 2009 15:23:10 +0100 | Christian Urban | smaller theory footprint | changeset | files |
| Fri, 04 Dec 2009 15:20:06 +0100 | Christian Urban | merged | changeset | files |
| Fri, 04 Dec 2009 15:19:39 +0100 | Christian Urban | merge | changeset | files |
| Fri, 04 Dec 2009 15:18:37 +0100 | Christian Urban | smaller theory footprint | changeset | files |
| Fri, 04 Dec 2009 15:18:33 +0100 | Cezary Kaliszyk | More name changes | changeset | files |
| Fri, 04 Dec 2009 15:04:05 +0100 | Cezary Kaliszyk | Naming changes | changeset | files |
| Fri, 04 Dec 2009 14:35:36 +0100 | Cezary Kaliszyk | code cleaning and renaming | changeset | files |
| Fri, 04 Dec 2009 14:11:20 +0100 | Cezary Kaliszyk | merge | changeset | files |
| Fri, 04 Dec 2009 14:11:03 +0100 | Cezary Kaliszyk | Removed previous inj_repabs_tac | changeset | files |
| Fri, 04 Dec 2009 13:58:23 +0100 | Christian Urban | some tuning | changeset | files |
| Fri, 04 Dec 2009 12:21:15 +0100 | Cezary Kaliszyk | merge | changeset | files |
| Fri, 04 Dec 2009 12:20:49 +0100 | Cezary Kaliszyk | rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification. | changeset | files |
| Fri, 04 Dec 2009 11:34:49 +0100 | Christian Urban | merged | changeset | files |
| Fri, 04 Dec 2009 11:34:21 +0100 | Christian Urban | merged | changeset | files |
| Fri, 04 Dec 2009 11:33:58 +0100 | Cezary Kaliszyk | Change equiv_trans2 to EQUALS_RSP, since we can prove it for any quotient type, not only for eqv relations. | changeset | files |
| Fri, 04 Dec 2009 11:06:43 +0100 | Cezary Kaliszyk | compose_tac instead of rtac to avoid unification; some code cleaning. | changeset | files |
| Fri, 04 Dec 2009 10:36:35 +0100 | Cezary Kaliszyk | Got to about 5 seconds for the longest proof. APPLY_RSP_TAC' solves the quotient internally without instantiation resulting in a faster proof. | changeset | files |
| Fri, 04 Dec 2009 10:12:17 +0100 | Cezary Kaliszyk | Using APPLY_RSP1; again a little bit faster. | changeset | files |
| Fri, 04 Dec 2009 09:33:32 +0100 | Cezary Kaliszyk | Fixes after big merge. | changeset | files |
| Fri, 04 Dec 2009 09:25:27 +0100 | Cezary Kaliszyk | The big merge; probably non-functional. | changeset | files |
| Fri, 04 Dec 2009 09:08:51 +0100 | Cezary Kaliszyk | Testing the new tactic everywhere | changeset | files |
| Fri, 04 Dec 2009 09:01:13 +0100 | Cezary Kaliszyk | First version of the deterministic rep-abs-inj-tac. | changeset | files |
| Fri, 04 Dec 2009 09:18:46 +0100 | Cezary Kaliszyk | Changing = to \<equiv> in case if we want to use simp. | changeset | files |
| Fri, 04 Dec 2009 09:10:31 +0100 | Cezary Kaliszyk | Even better: Completely got rid of the simps in both quotient_tac and inj_repabs_tac | changeset | files |
| Fri, 04 Dec 2009 08:19:56 +0100 | Cezary Kaliszyk | merge | changeset | files |
| Fri, 04 Dec 2009 08:18:38 +0100 | Cezary Kaliszyk | Made your version work again with LIST_REL_EQ. | changeset | files |
| Thu, 03 Dec 2009 19:06:14 +0100 | Christian Urban | the error occurs in APPLY_RSP_TAC where the wrong quotient (for LIST_REL) is applied | changeset | files |
| Thu, 03 Dec 2009 15:03:31 +0100 | Christian Urban | removed quot argument...not all examples work anymore | changeset | files |
| Thu, 03 Dec 2009 14:02:05 +0100 | Christian Urban | merged | changeset | files |
| Thu, 03 Dec 2009 14:00:43 +0100 | Christian Urban | merged | changeset | files |
| Thu, 03 Dec 2009 13:59:53 +0100 | Christian Urban | first version of internalised quotient theorems; added FIXME-TODO | changeset | files |
| Thu, 03 Dec 2009 11:40:10 +0100 | Christian Urban | further dead code | changeset | files |
| Thu, 03 Dec 2009 13:56:59 +0100 | Cezary Kaliszyk | Reintroduced varifyT; we still need it for permutation definition. | changeset | files |
| Thu, 03 Dec 2009 13:45:52 +0100 | Cezary Kaliszyk | Updated the examples | changeset | files |
| Thu, 03 Dec 2009 12:33:05 +0100 | Cezary Kaliszyk | Fixed previous mistake | changeset | files |
| Thu, 03 Dec 2009 12:31:05 +0100 | Cezary Kaliszyk | defs used automatically by clean_tac | changeset | files |
| Thu, 03 Dec 2009 12:22:19 +0100 | Cezary Kaliszyk | Added qoutient_consts dest for getting all the constant definitions in the cleaning step. | changeset | files |
| Thu, 03 Dec 2009 12:17:23 +0100 | Cezary Kaliszyk | Added the definition to quotient constant data. | changeset | files |
| Thu, 03 Dec 2009 11:58:46 +0100 | Cezary Kaliszyk | removing unused code | changeset | files |
| Thu, 03 Dec 2009 11:34:34 +0100 | Christian Urban | merged | changeset | files |
| Thu, 03 Dec 2009 11:33:24 +0100 | Christian Urban | deleted some dead code | changeset | files |
| Thu, 03 Dec 2009 11:28:19 +0100 | Cezary Kaliszyk | Included all_prs and ex_prs in the lambda_prs conversion. | changeset | files |
| Thu, 03 Dec 2009 02:53:54 +0100 | Christian Urban | further simplification | changeset | files |
| Thu, 03 Dec 2009 02:18:21 +0100 | Christian Urban | simplified lambda_prs_conv | changeset | files |
| Wed, 02 Dec 2009 23:31:30 +0100 | Christian Urban | deleted now obsolete argument rty everywhere | changeset | files |
| Wed, 02 Dec 2009 23:11:50 +0100 | Christian Urban | deleted tests at the beginning of QuotMain | changeset | files |
| Wed, 02 Dec 2009 20:54:59 +0100 | Cezary Kaliszyk | Experiments with OPTION_map | changeset | files |
| Wed, 02 Dec 2009 17:16:44 +0100 | Cezary Kaliszyk | merge | changeset | files |
| Wed, 02 Dec 2009 17:15:36 +0100 | Cezary Kaliszyk | More experiments with higher order quotients and theorems with non-lifted constants. | changeset | files |
| Wed, 02 Dec 2009 16:12:41 +0100 | Christian Urban | merged | changeset | files |
| Wed, 02 Dec 2009 14:37:21 +0100 | Cezary Kaliszyk | Lifting to 2 different types :) | changeset | files |
| Wed, 02 Dec 2009 14:11:46 +0100 | Cezary Kaliszyk | New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet. | changeset | files |