QuotMain.thy
2009-12-03 Christian Urban simplified lambda_prs_conv
2009-12-02 Christian Urban deleted now obsolete argument rty everywhere
2009-12-02 Christian Urban deleted tests at the beginning of QuotMain
2009-12-02 Cezary Kaliszyk Experiments with OPTION_map
2009-12-02 Cezary Kaliszyk merge
2009-12-02 Cezary Kaliszyk More experiments with higher order quotients and theorems with non-lifted constants.
2009-12-02 Christian Urban merged
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 Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
2009-12-01 Cezary Kaliszyk back in working state
2009-12-01 Cezary Kaliszyk clean
2009-12-01 Christian Urban fixed previous commit
2009-12-01 Christian Urban fixed problems with FOCUS
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 Removed last HOL_ss
2009-12-01 Cezary Kaliszyk more cleaning
2009-12-01 Cezary Kaliszyk Cleaning 'aps'.
2009-11-30 Cezary Kaliszyk merge
2009-11-30 Christian Urban cleaned inj_regabs_trm
2009-11-30 Cezary Kaliszyk merge
2009-11-30 Cezary Kaliszyk clean_tac rewrites the definitions the other way
2009-11-30 Christian Urban merged
2009-11-30 Christian Urban added facilities to get all stored quotient data (equiv thms etc)
2009-11-30 Cezary Kaliszyk More code cleaning
2009-11-30 Cezary Kaliszyk Code cleaning.
2009-11-30 Cezary Kaliszyk Commented clean-tac
2009-11-29 Christian Urban tried to improve the inj_repabs_trm function but left the new part commented out
2009-11-29 Christian Urban started functions for qid-insertion and fixed a bug in regularise
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-29 Christian Urban tuned
2009-11-28 Christian Urban improved pattern matching inside the inj_repabs_tacs
2009-11-28 Christian Urban selective debugging of the inj_repabs_tac (at the moment for step 3 and 4 debugging information is printed)
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 tuning
2009-11-28 Christian Urban tuned comments
2009-11-28 Christian Urban renamed LAMBDA_RES_TAC and WEAK_LAMBDA_RES_TAC to lower case names
2009-11-28 Cezary Kaliszyk Moved fast instantiation to QuotMain
2009-11-28 Christian Urban further proper merge
2009-11-28 Christian Urban merged
2009-11-28 Christian Urban more simplification
less more (0) -300 -100 -48 tip