| Mon, 07 Dec 2009 12:14:25 +0100 |
Cezary Kaliszyk |
Fix of regularize for babs and proof of babs_rsp.
|
file |
diff |
annotate
|
| Mon, 07 Dec 2009 08:45:04 +0100 |
Cezary Kaliszyk |
QuotProd with product_quotient and a 3 respects and preserves lemmas.
|
file |
diff |
annotate
|
| Sat, 05 Dec 2009 21:28:24 +0100 |
Cezary Kaliszyk |
Solutions to IntEx tests.
|
file |
diff |
annotate
|
| Fri, 04 Dec 2009 18:32:19 +0100 |
Cezary Kaliszyk |
abs_rep as ==
|
file |
diff |
annotate
|
| Fri, 04 Dec 2009 17:36:45 +0100 |
Cezary Kaliszyk |
Cleaning/review of QuotScript.
|
file |
diff |
annotate
|
| Fri, 04 Dec 2009 17:15:55 +0100 |
Cezary Kaliszyk |
More cleaning
|
file |
diff |
annotate
|
| Fri, 04 Dec 2009 16:53:11 +0100 |
Cezary Kaliszyk |
more name cleaning and removing
|
file |
diff |
annotate
|
| Fri, 04 Dec 2009 16:40:23 +0100 |
Cezary Kaliszyk |
More code cleaning and renaming: moved rsp and prs lemmas from Int to QuotList
|
file |
diff |
annotate
|
| Fri, 04 Dec 2009 16:12:40 +0100 |
Cezary Kaliszyk |
Cleaning & Renaming coming from QuotList
|
file |
diff |
annotate
|
| Fri, 04 Dec 2009 15:50:57 +0100 |
Cezary Kaliszyk |
Even more name changes and cleaning
|
file |
diff |
annotate
|
| Fri, 04 Dec 2009 15:41:09 +0100 |
Cezary Kaliszyk |
More code cleaning and name changes
|
file |
diff |
annotate
|
| Fri, 04 Dec 2009 15:18:37 +0100 |
Christian Urban |
smaller theory footprint
|
file |
diff |
annotate
|
| Fri, 04 Dec 2009 15:04:05 +0100 |
Cezary Kaliszyk |
Naming changes
|
file |
diff |
annotate
|
| Fri, 04 Dec 2009 14:35:36 +0100 |
Cezary Kaliszyk |
code cleaning and renaming
|
file |
diff |
annotate
|
| 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.
|
file |
diff |
annotate
|
| Fri, 04 Dec 2009 10:12:17 +0100 |
Cezary Kaliszyk |
Using APPLY_RSP1; again a little bit faster.
|
file |
diff |
annotate
|
| Fri, 04 Dec 2009 09:33:32 +0100 |
Cezary Kaliszyk |
Fixes after big merge.
|
file |
diff |
annotate
|
| Fri, 04 Dec 2009 09:18:46 +0100 |
Cezary Kaliszyk |
Changing = to \<equiv> in case if we want to use simp.
|
file |
diff |
annotate
|
| Mon, 30 Nov 2009 12:14:20 +0100 |
Cezary Kaliszyk |
More code cleaning
|
file |
diff |
annotate
|
| Mon, 30 Nov 2009 11:53:20 +0100 |
Cezary Kaliszyk |
Code cleaning.
|
file |
diff |
annotate
|
| Sat, 28 Nov 2009 05:29:30 +0100 |
Cezary Kaliszyk |
Finished and tested the new regularize
|
file |
diff |
annotate
|
| Sat, 28 Nov 2009 04:02:54 +0100 |
Cezary Kaliszyk |
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
|
file |
diff |
annotate
|
| Fri, 27 Nov 2009 08:15:23 +0100 |
Cezary Kaliszyk |
Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
|
file |
diff |
annotate
|
| Thu, 26 Nov 2009 13:52:46 +0100 |
Christian Urban |
fixed QuotList
|
file |
diff |
annotate
|