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