LFex.thy
2009-12-05 Christian Urban simplified inj_repabs_trm
2009-12-04 Cezary Kaliszyk more name cleaning and removing
2009-12-04 Cezary Kaliszyk merged
2009-12-04 Christian Urban merge
2009-12-04 Cezary Kaliszyk Removed previous inj_repabs_tac
2009-12-04 Cezary Kaliszyk rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
2009-12-04 Cezary Kaliszyk Using APPLY_RSP1; again a little bit faster.
2009-12-04 Cezary Kaliszyk The big merge; probably non-functional.
2009-12-04 Cezary Kaliszyk Testing the new tactic everywhere
2009-12-04 Cezary Kaliszyk First version of the deterministic rep-abs-inj-tac.
2009-12-03 Christian Urban removed quot argument...not all examples work anymore
2009-12-03 Cezary Kaliszyk Reintroduced varifyT; we still need it for permutation definition.
2009-12-03 Cezary Kaliszyk Updated the examples
2009-12-03 Cezary Kaliszyk Added the definition to quotient constant data.
2009-12-03 Cezary Kaliszyk Included all_prs and ex_prs in the lambda_prs conversion.
2009-12-02 Christian Urban deleted now obsolete argument rty everywhere
2009-12-02 Cezary Kaliszyk Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
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 Code cleaning.
2009-11-30 Cezary Kaliszyk Added another induction to LFex
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 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 Manually finished LF induction.
2009-11-28 Cezary Kaliszyk Moved fast instantiation to QuotMain
2009-11-28 Cezary Kaliszyk LFex proof a bit further.
2009-11-28 Cezary Kaliszyk Looking at repabs proof in LF.
2009-11-28 Cezary Kaliszyk Finished and tested the new regularize
2009-11-28 Cezary Kaliszyk Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
2009-11-28 Cezary Kaliszyk Integrated Stefan's tactic and changed substs to simps with empty context.
2009-11-27 Cezary Kaliszyk The magical code from Stefan, will need to be integrated in the Simproc.
2009-11-27 Cezary Kaliszyk Simplifying arguments; got rid of trans2_thm.
2009-11-27 Cezary Kaliszyk Cleaning of LFex. Lambda_prs fails to unify in 2 places.
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 Merged
2009-11-26 Christian Urban introduced a new property for Ball and ===> on the left
2009-11-26 Cezary Kaliszyk Manually regularized akind_aty_atrm.induct
2009-11-26 Cezary Kaliszyk Playing with Monos in LFex.
2009-11-09 Cezary Kaliszyk Cleaning and commenting
2009-11-06 Christian Urban permutation lifting works now also
2009-11-06 Christian Urban updated to new Isabelle version and added a new example file
less more (0) tip