| Sun, 29 Nov 2009 23:59:37 +0100 |
Christian Urban |
tried to improve the inj_repabs_trm function but left the new part commented out
|
file |
diff |
annotate
|
| Sun, 29 Nov 2009 08:48:06 +0100 |
Cezary Kaliszyk |
Added 'TRY' to refl in clean_tac to get as far as possible. Removed unnecessary [quot_rsp] in FSet. Added necessary [quot_rsp] and one lifted thm in LamEx.
|
file |
diff |
annotate
|
| Sun, 29 Nov 2009 03:59:18 +0100 |
Christian Urban |
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
|
file |
diff |
annotate
|
| Sat, 28 Nov 2009 14:45:22 +0100 |
Christian Urban |
removed old inj_repabs_tac; kept only the one with (selective) debugging information
|
file |
diff |
annotate
|
| Sat, 28 Nov 2009 14:33:04 +0100 |
Christian Urban |
renamed r_mk_comb_tac to inj_repabs_tac
|
file |
diff |
annotate
|
| Sat, 28 Nov 2009 05:43:18 +0100 |
Cezary Kaliszyk |
Merged and tested that all works.
|
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:46:03 +0100 |
Christian Urban |
fixed examples in IntEx and FSet
|
file |
diff |
annotate
|
| Sat, 28 Nov 2009 04:37:04 +0100 |
Christian Urban |
fixed previous commit
|
file |
diff |
annotate
|
| Sat, 28 Nov 2009 02:54:24 +0100 |
Christian Urban |
annotated a proof with all steps and simplified LAMBDA_RES_TAC
|
file |
diff |
annotate
|
| Fri, 27 Nov 2009 10:04:49 +0100 |
Cezary Kaliszyk |
Simplifying arguments; got rid of trans2_thm.
|
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
|
| Fri, 27 Nov 2009 07:00:14 +0100 |
Cezary Kaliszyk |
Minor cleaning
|
file |
diff |
annotate
|
| Fri, 27 Nov 2009 02:55:56 +0100 |
Christian Urban |
introduced a separate lemma for id_simps
|
file |
diff |
annotate
|
| Fri, 27 Nov 2009 02:35:50 +0100 |
Christian Urban |
deleted obsolete qenv code
|
file |
diff |
annotate
|