nominal2: File revisions

QuotScript.thy

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
2009-10-24	Cezary Kaliszyk	More infrastructure for automatic lifting of theorems lifted before	file \| diff \| annotate
2009-10-24	cek	Better tactic and simplified the proof further	file \| diff \| annotate
2009-10-23	Cezary Kaliszyk	eqsubst_tac	file \| diff \| annotate
2009-10-22	Cezary Kaliszyk	Removed an assumption	file \| diff \| annotate
2009-10-22	Cezary Kaliszyk	The proof now including manually unfolded higher-order RES_FORALL_RSP.	file \| diff \| annotate

nominal2