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
|