FSet.thy
2009-12-02 Christian Urban deleted now obsolete argument rty everywhere
2009-12-02 Cezary Kaliszyk Lifting to 2 different types :)
2009-12-02 Cezary Kaliszyk New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
2009-12-02 Cezary Kaliszyk Fixed unlam for non-abstractions and updated list_induct_part proof.
2009-12-02 Cezary Kaliszyk Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
2009-12-02 Cezary Kaliszyk The conversion approach works.
2009-12-02 Cezary Kaliszyk Trying a conversion based approach.
2009-12-02 Cezary Kaliszyk A bit of progress; but the object-logic vs meta-logic distinction is troublesome.
2009-12-01 Cezary Kaliszyk back in working state
2009-12-01 Cezary Kaliszyk clean
2009-12-01 Christian Urban added a make_inst test
2009-12-01 Cezary Kaliszyk Transformation of QUOT_TRUE assumption by any given function
2009-12-01 Christian Urban QUOT_TRUE joke
2009-12-01 Cezary Kaliszyk more cleaning
2009-12-01 Cezary Kaliszyk Cleaning 'aps'.
2009-11-30 Cezary Kaliszyk clean_tac rewrites the definitions the other way
2009-11-30 Cezary Kaliszyk More code cleaning
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 Removed unnecessary HOL_ss which proved one of the subgoals.
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 improved pattern matching inside the inj_repabs_tacs
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 Christian Urban renamed LAMBDA_RES_TAC and WEAK_LAMBDA_RES_TAC to lower case names
2009-11-28 Christian Urban merged
2009-11-28 Christian Urban more simplification
2009-11-28 Cezary Kaliszyk Merged and tested that all works.
2009-11-28 Cezary Kaliszyk Finished and tested the new regularize
less more (0) -100 -50 -30 tip