2009-12-07 |
Cezary Kaliszyk |
inj_repabs_tac handles Babs now.
|
file |
diff |
annotate
|
2009-12-07 |
Cezary Kaliszyk |
Using pair_prs; debugging the error in regularize of a lambda.
|
file |
diff |
annotate
|
2009-12-07 |
Cezary Kaliszyk |
QuotProd with product_quotient and a 3 respects and preserves lemmas.
|
file |
diff |
annotate
|
2009-12-07 |
Cezary Kaliszyk |
merge
|
file |
diff |
annotate
|
2009-12-07 |
Cezary Kaliszyk |
3 new example thms in MyInt; reveal problems with handling of lambdas; regularize fails with "Loose Bound".
|
file |
diff |
annotate
|
2009-12-07 |
Christian Urban |
removed usage of HOL_basic_ss by using a slighly extended version of empty_ss
|
file |
diff |
annotate
|
2009-12-06 |
Christian Urban |
fixed examples
|
file |
diff |
annotate
|
2009-12-06 |
Christian Urban |
added a theorem list for equivalence theorems
|
file |
diff |
annotate
|
2009-12-06 |
Christian Urban |
working on lambda_prs with examples; polished code of clean_tac
|
file |
diff |
annotate
|
2009-12-05 |
Christian Urban |
merged
|
file |
diff |
annotate
|
2009-12-05 |
Christian Urban |
added new example for Ints; regularise does not work in all instances
|
file |
diff |
annotate
|
2009-12-05 |
Cezary Kaliszyk |
Proved foldl_rsp and ho_map_rsp
|
file |
diff |
annotate
|
2009-12-05 |
Christian Urban |
moved all_prs and ex_prs out from the conversion into the simplifier
|
file |
diff |
annotate
|
2009-12-05 |
Cezary Kaliszyk |
Added nil_rsp and cons_rsp to quotient_rsp; simplified IntEx.
|
file |
diff |
annotate
|
2009-12-05 |
Christian Urban |
merged
|
file |
diff |
annotate
|
2009-12-05 |
Christian Urban |
merged
|
file |
diff |
annotate
|
2009-12-05 |
Christian Urban |
merged
|
file |
diff |
annotate
|
2009-12-05 |
Christian Urban |
simpler version of clean_tac
|
file |
diff |
annotate
|
2009-12-05 |
Cezary Kaliszyk |
Handling of respects in the fast inj_repabs_tac; includes respects with quotient assumptions.
|
file |
diff |
annotate
|
2009-12-05 |
Cezary Kaliszyk |
Solutions to IntEx tests.
|
file |
diff |
annotate
|
2009-12-05 |
Christian Urban |
made some slight simplifications to the examples
|
file |
diff |
annotate
|
2009-12-05 |
Christian Urban |
added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet
|
file |
diff |
annotate
|
2009-12-04 |
Christian Urban |
not yet quite functional treatment of constants
|
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 |
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 |
Cezary Kaliszyk |
More name changes
|
file |
diff |
annotate
|
2009-12-03 |
Christian Urban |
removed quot argument...not all examples work anymore
|
file |
diff |
annotate
|
2009-12-03 |
Christian Urban |
merged
|
file |
diff |
annotate
|
2009-12-03 |
Christian Urban |
merged
|
file |
diff |
annotate
|
2009-12-03 |
Cezary Kaliszyk |
Updated the examples
|
file |
diff |
annotate
|
2009-12-03 |
Christian Urban |
merged
|
file |
diff |
annotate
|
2009-12-03 |
Christian Urban |
deleted some dead code
|
file |
diff |
annotate
|
2009-12-02 |
Christian Urban |
deleted now obsolete argument rty everywhere
|
file |
diff |
annotate
|
2009-12-02 |
Cezary Kaliszyk |
More experiments with higher order quotients and theorems with non-lifted constants.
|
file |
diff |
annotate
|
2009-12-01 |
Cezary Kaliszyk |
Cleaning 'aps'.
|
file |
diff |
annotate
|
2009-11-30 |
Cezary Kaliszyk |
Code cleaning.
|
file |
diff |
annotate
|
2009-11-29 |
Christian Urban |
tried to improve the inj_repabs_trm function but left the new part commented out
|
file |
diff |
annotate
|
2009-11-29 |
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
|
2009-11-29 |
Christian Urban |
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
|
file |
diff |
annotate
|
2009-11-28 |
Christian Urban |
removed old inj_repabs_tac; kept only the one with (selective) debugging information
|
file |
diff |
annotate
|
2009-11-28 |
Christian Urban |
renamed r_mk_comb_tac to inj_repabs_tac
|
file |
diff |
annotate
|
2009-11-28 |
Cezary Kaliszyk |
Merged and tested that all works.
|
file |
diff |
annotate
|
2009-11-28 |
Cezary Kaliszyk |
Finished and tested the new regularize
|
file |
diff |
annotate
|
2009-11-28 |
Christian Urban |
fixed examples in IntEx and FSet
|
file |
diff |
annotate
|
2009-11-28 |
Christian Urban |
fixed previous commit
|
file |
diff |
annotate
|
2009-11-28 |
Christian Urban |
annotated a proof with all steps and simplified LAMBDA_RES_TAC
|
file |
diff |
annotate
|
2009-11-27 |
Cezary Kaliszyk |
Simplifying arguments; got rid of trans2_thm.
|
file |
diff |
annotate
|