nominal2: File revisions

Mercurial Mercurial > hg > nominal2 / file revisions

summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -16 tip

QuotScript.thy

2009-11-28	Cezary Kaliszyk	Finished and tested the new regularize	file \| diff \| annotate
2009-11-28	Cezary Kaliszyk	Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.	file \| diff \| annotate
2009-11-27	Cezary Kaliszyk	Removing arguments of tactics: absrep, rel_refl, reps_same are computed.	file \| diff \| annotate
2009-11-26	Christian Urban	fixed QuotList	file \| diff \| annotate
2009-11-26	Christian Urban	changed left-res	file \| diff \| annotate
2009-11-26	Cezary Kaliszyk	Manually regularized akind_aty_atrm.induct	file \| diff \| annotate
2009-11-13	Cezary Kaliszyk	Still don't know how to do the proof automatically.	file \| diff \| annotate
2009-10-31	Cezary Kaliszyk	Automatic computation of application preservation and manually finished "alpha.induct". Slow...	file \| diff \| annotate
2009-10-30	Cezary Kaliszyk	Regularize for equalities and a better tactic. "alpha.cases" now lifts.	file \| diff \| annotate
2009-10-28	Cezary Kaliszyk	disambiguate ===> syntax	file \| diff \| annotate
2009-10-28	Cezary Kaliszyk	First experiments with Lambda	file \| diff \| annotate
2009-10-26	Cezary Kaliszyk	Finished COND_PRS proof.	file \| diff \| annotate
2009-10-26	Cezary Kaliszyk	Cleaning and fixing.	file \| diff \| annotate
2009-10-24	Christian Urban	proved the two lemmas in QuotScript (reformulated them without leading forall)	file \| diff \| annotate
2009-10-24	Cezary Kaliszyk	Finally completely lift the previously lifted theorems + clean some old stuff	file \| diff \| annotate
2009-10-24	Cezary Kaliszyk	More infrastructure for automatic lifting of theorems lifted before	file \| diff \| annotate

less more (0) -16 tip

nominal2