FSet.thy
2009-12-04 Cezary Kaliszyk More code cleaning and name changes
2009-12-04 Cezary Kaliszyk More name changes
2009-12-04 Cezary Kaliszyk merge
2009-12-04 Cezary Kaliszyk Removed previous inj_repabs_tac
2009-12-04 Christian Urban some tuning
2009-12-04 Cezary Kaliszyk Using APPLY_RSP1; again a little bit faster.
2009-12-04 Cezary Kaliszyk merge
2009-12-04 Cezary Kaliszyk Made your version work again with LIST_REL_EQ.
2009-12-03 Christian Urban the error occurs in APPLY_RSP_TAC where the wrong quotient (for LIST_REL) is applied
2009-12-03 Christian Urban removed quot argument...not all examples work anymore
2009-12-03 Cezary Kaliszyk defs used automatically by clean_tac
2009-12-03 Cezary Kaliszyk Added the definition to quotient constant data.
2009-12-03 Cezary Kaliszyk removing unused code
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
2009-11-28 Christian Urban fixed examples in IntEx and FSet
2009-11-28 Christian Urban annotated a proof with all steps and simplified LAMBDA_RES_TAC
2009-11-27 Christian Urban replaced FIRST' (map rtac list) with resolve_tac list
2009-11-27 Cezary Kaliszyk Simplifying arguments; got rid of trans2_thm.
2009-11-27 Cezary Kaliszyk Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
2009-11-27 Cezary Kaliszyk Minor cleaning
2009-11-26 Cezary Kaliszyk Merge Again
2009-11-26 Cezary Kaliszyk Merged
2009-11-26 Christian Urban tuned comments
2009-11-26 Christian Urban some diagnostic code for r_mk_comb
2009-11-26 Christian Urban introduced a new property for Ball and ===> on the left
2009-11-26 Christian Urban changed left-res
2009-11-26 Cezary Kaliszyk Fixed FSet after merge.
2009-11-26 Christian Urban merged
2009-11-26 Christian Urban test with monos
2009-11-25 Cezary Kaliszyk applic_prs
2009-11-25 Christian Urban reordered the code
less more (0) -100 -60 tip