2009-12-05 |
Cezary Kaliszyk |
Solutions to IntEx tests.
|
file |
diff |
annotate
|
2009-12-04 |
Cezary Kaliszyk |
abs_rep as ==
|
file |
diff |
annotate
|
2009-12-04 |
Cezary Kaliszyk |
Cleaning/review of QuotScript.
|
file |
diff |
annotate
|
2009-12-04 |
Cezary Kaliszyk |
More cleaning
|
file |
diff |
annotate
|
2009-12-04 |
Cezary Kaliszyk |
more name cleaning and removing
|
file |
diff |
annotate
|
2009-12-04 |
Cezary Kaliszyk |
More code cleaning and renaming: moved rsp and prs lemmas from Int to QuotList
|
file |
diff |
annotate
|
2009-12-04 |
Cezary Kaliszyk |
Cleaning & Renaming coming from QuotList
|
file |
diff |
annotate
|
2009-12-04 |
Cezary Kaliszyk |
Even more name changes and cleaning
|
file |
diff |
annotate
|
2009-12-04 |
Cezary Kaliszyk |
More code cleaning and name changes
|
file |
diff |
annotate
|
2009-12-04 |
Christian Urban |
smaller theory footprint
|
file |
diff |
annotate
|
2009-12-04 |
Cezary Kaliszyk |
Naming changes
|
file |
diff |
annotate
|
2009-12-04 |
Cezary Kaliszyk |
code cleaning and renaming
|
file |
diff |
annotate
|
2009-12-04 |
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
|
2009-12-04 |
Cezary Kaliszyk |
Using APPLY_RSP1; again a little bit faster.
|
file |
diff |
annotate
|
2009-12-04 |
Cezary Kaliszyk |
Fixes after big merge.
|
file |
diff |
annotate
|
2009-12-04 |
Cezary Kaliszyk |
Changing = to \<equiv> in case if we want to use simp.
|
file |
diff |
annotate
|
2009-11-30 |
Cezary Kaliszyk |
More code cleaning
|
file |
diff |
annotate
|
2009-11-30 |
Cezary Kaliszyk |
Code cleaning.
|
file |
diff |
annotate
|
2009-11-28 |
Cezary Kaliszyk |
Finished and tested the new regularize
|
file |
diff |
annotate
|
2009-11-28 |
Cezary Kaliszyk |
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
|
file |
diff |
annotate
|
2009-11-27 |
Cezary Kaliszyk |
Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
|
file |
diff |
annotate
|
2009-11-26 |
Christian Urban |
fixed QuotList
|
file |
diff |
annotate
|
2009-11-26 |
Christian Urban |
changed left-res
|
file |
diff |
annotate
|
2009-11-26 |
Cezary Kaliszyk |
Manually regularized akind_aty_atrm.induct
|
file |
diff |
annotate
|
2009-11-13 |
Cezary Kaliszyk |
Still don't know how to do the proof automatically.
|
file |
diff |
annotate
|
2009-10-31 |
Cezary Kaliszyk |
Automatic computation of application preservation and manually finished "alpha.induct". Slow...
|
file |
diff |
annotate
|
2009-10-30 |
Cezary Kaliszyk |
Regularize for equalities and a better tactic. "alpha.cases" now lifts.
|
file |
diff |
annotate
|
2009-10-28 |
Cezary Kaliszyk |
disambiguate ===> syntax
|
file |
diff |
annotate
|
2009-10-28 |
Cezary Kaliszyk |
First experiments with Lambda
|
file |
diff |
annotate
|
2009-10-26 |
Cezary Kaliszyk |
Finished COND_PRS proof.
|
file |
diff |
annotate
|
2009-10-26 |
Cezary Kaliszyk |
Cleaning and fixing.
|
file |
diff |
annotate
|
2009-10-24 |
Christian Urban |
proved the two lemmas in QuotScript (reformulated them without leading forall)
|
file |
diff |
annotate
|
2009-10-24 |
Cezary Kaliszyk |
Finally completely lift the previously lifted theorems + clean some old stuff
|
file |
diff |
annotate
|
2009-10-24 |
Cezary Kaliszyk |
More infrastructure for automatic lifting of theorems lifted before
|
file |
diff |
annotate
|
2009-10-24 |
Cezary Kaliszyk |
More infrastructure for automatic lifting of theorems lifted before
|
file |
diff |
annotate
|
2009-10-24 |
cek |
Better tactic and simplified the proof further
|
file |
diff |
annotate
|
2009-10-23 |
Cezary Kaliszyk |
eqsubst_tac
|
file |
diff |
annotate
|
2009-10-22 |
Cezary Kaliszyk |
Removed an assumption
|
file |
diff |
annotate
|
2009-10-22 |
Cezary Kaliszyk |
The proof now including manually unfolded higher-order RES_FORALL_RSP.
|
file |
diff |
annotate
|
2009-10-22 |
Cezary Kaliszyk |
The problems with 'abs' term.
|
file |
diff |
annotate
|
2009-10-17 |
Cezary Kaliszyk |
Partial simplification of the proof
|
file |
diff |
annotate
|
2009-10-16 |
Cezary Kaliszyk |
Symmetric version of REP_ABS_RSP
|
file |
diff |
annotate
|
2009-10-16 |
Cezary Kaliszyk |
Progressing with the proof
|
file |
diff |
annotate
|
2009-10-15 |
Cezary Kaliszyk |
A number of lemmas for REGULARIZE_TAC and regularizing card1.
|
file |
diff |
annotate
|
2009-10-14 |
Cezary Kaliszyk |
Proving the proper RepAbs version
|
file |
diff |
annotate
|
2009-10-14 |
Cezary Kaliszyk |
Manually regularized list_induct2
|
file |
diff |
annotate
|
2009-08-11 |
Christian Urban |
initial commit
|
file |
diff |
annotate
|