Mercurial Mercurial > hg > nominal2 / shortlog
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -300 -100 -50 -30 +30 +50 +100 +300 +1000 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
 
2009-11-30 Cezary Kaliszyk clean_tac rewrites the definitions the other way changeset | files
2009-11-30 Christian Urban merged changeset | files
2009-11-30 Christian Urban added facilities to get all stored quotient data (equiv thms etc) changeset | files
2009-11-30 Cezary Kaliszyk More code cleaning changeset | files
2009-11-30 Cezary Kaliszyk Code cleaning. changeset | files
2009-11-30 Cezary Kaliszyk Commented clean-tac changeset | files
2009-11-30 Cezary Kaliszyk Added another induction to LFex changeset | files
2009-11-29 Christian Urban tried to improve the inj_repabs_trm function but left the new part commented out changeset | files
2009-11-29 Christian Urban added a new version of QuotMain to experiment with qids changeset | files
2009-11-29 Christian Urban started functions for qid-insertion and fixed a bug in regularise changeset | files
2009-11-29 Cezary Kaliszyk Removed unnecessary HOL_ss which proved one of the subgoals. changeset | files
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. changeset | files
2009-11-29 Christian Urban introduced a global list of respectfulness lemmas; the attribute is [quot_rsp] changeset | files
2009-11-29 Christian Urban tuned changeset | files
2009-11-28 Christian Urban improved pattern matching inside the inj_repabs_tacs changeset | files
2009-11-28 Christian Urban selective debugging of the inj_repabs_tac (at the moment for step 3 and 4 debugging information is printed) changeset | files
2009-11-28 Christian Urban removed old inj_repabs_tac; kept only the one with (selective) debugging information changeset | files
2009-11-28 Christian Urban renamed r_mk_comb_tac to inj_repabs_tac changeset | files
2009-11-28 Christian Urban tuning changeset | files
2009-11-28 Christian Urban tuned comments changeset | files
2009-11-28 Christian Urban renamed LAMBDA_RES_TAC and WEAK_LAMBDA_RES_TAC to lower case names changeset | files
2009-11-28 Cezary Kaliszyk Manually finished LF induction. changeset | files
2009-11-28 Cezary Kaliszyk Moved fast instantiation to QuotMain changeset | files
2009-11-28 Cezary Kaliszyk LFex proof a bit further. changeset | files
2009-11-28 Cezary Kaliszyk merge changeset | files
2009-11-28 Cezary Kaliszyk Looking at repabs proof in LF. changeset | files
2009-11-28 Christian Urban further proper merge changeset | files
2009-11-28 Christian Urban merged changeset | files
2009-11-28 Christian Urban more simplification changeset | files
2009-11-28 Cezary Kaliszyk Merged and tested that all works. changeset | files
(0) -300 -100 -50 -30 +30 +50 +100 +300 +1000 tip
nominal2