| Fri, 04 Dec 2009 18:32:19 +0100 | Cezary Kaliszyk | abs_rep as == | changeset | files |
| Fri, 04 Dec 2009 17:57:03 +0100 | Cezary Kaliszyk | Cleaning the Quotients file | changeset | files |
| Fri, 04 Dec 2009 17:50:02 +0100 | Cezary Kaliszyk | Minor renames and moving | changeset | files |
| Fri, 04 Dec 2009 17:36:45 +0100 | Cezary Kaliszyk | Cleaning/review of QuotScript. | changeset | files |
| Fri, 04 Dec 2009 17:15:55 +0100 | Cezary Kaliszyk | More cleaning | changeset | files |
| 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 |