LFex.thy
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