nominal2: File revisions

QuotScript.thy

Sun, 25 Oct 2009 01:15:03 +0200	Christian Urban	proved the two lemmas in QuotScript (reformulated them without leading forall)	file \| diff \| annotate
Sat, 24 Oct 2009 14:00:18 +0200	Cezary Kaliszyk	Finally completely lift the previously lifted theorems + clean some old stuff	file \| diff \| annotate
Sat, 24 Oct 2009 13:00:54 +0200	Cezary Kaliszyk	More infrastructure for automatic lifting of theorems lifted before	file \| diff \| annotate
Sat, 24 Oct 2009 10:16:53 +0200	Cezary Kaliszyk	More infrastructure for automatic lifting of theorems lifted before	file \| diff \| annotate
Sat, 24 Oct 2009 08:09:09 +0200	cek	Better tactic and simplified the proof further	file \| diff \| annotate
Fri, 23 Oct 2009 16:01:13 +0200	Cezary Kaliszyk	eqsubst_tac	file \| diff \| annotate
Thu, 22 Oct 2009 15:44:16 +0200	Cezary Kaliszyk	Removed an assumption	file \| diff \| annotate
Thu, 22 Oct 2009 15:02:01 +0200	Cezary Kaliszyk	The proof now including manually unfolded higher-order RES_FORALL_RSP.	file \| diff \| annotate

nominal2