QuotScript.thy
2009-12-04 Cezary Kaliszyk Naming changes
2009-12-04 Cezary Kaliszyk code cleaning and renaming
2009-12-04 Cezary Kaliszyk Change equiv_trans2 to EQUALS_RSP, since we can prove it for any quotient type, not only for eqv relations.
2009-12-04 Cezary Kaliszyk Using APPLY_RSP1; again a little bit faster.
2009-12-04 Cezary Kaliszyk Fixes after big merge.
2009-12-04 Cezary Kaliszyk Changing = to \<equiv> in case if we want to use simp.
2009-11-30 Cezary Kaliszyk More code cleaning
2009-11-30 Cezary Kaliszyk Code cleaning.
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-27 Cezary Kaliszyk Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
2009-11-26 Christian Urban fixed QuotList
2009-11-26 Christian Urban changed left-res
2009-11-26 Cezary Kaliszyk Manually regularized akind_aty_atrm.induct
less more (0) -14 tip