nominal2: File revisions

QuotMain.thy

2009-10-15	Cezary Kaliszyk	A number of lemmas for REGULARIZE_TAC and regularizing card1.	file \| diff \| annotate
2009-10-14	Cezary Kaliszyk	Proving the proper RepAbs version	file \| diff \| annotate
2009-10-14	Cezary Kaliszyk	Forgot to save, second part of the commit	file \| diff \| annotate
2009-10-14	Cezary Kaliszyk	Manually regularized list_induct2	file \| diff \| annotate
2009-10-14	Cezary Kaliszyk	Fixed bug in regularise types. Now we can regularise list.induct.	file \| diff \| annotate
2009-10-14	Cezary Kaliszyk	Function for checking recursively if lifting is needed	file \| diff \| annotate
2009-10-14	Cezary Kaliszyk	Merge	file \| diff \| annotate
2009-10-14	Cezary Kaliszyk	Proper handling of non-lifted quantifiers, testing type freezing.	file \| diff \| annotate
2009-10-13	Christian Urban	slight simplification of atomize_thm	file \| diff \| annotate
2009-10-13	Cezary Kaliszyk	atomize_thm and meta_quantify.	file \| diff \| annotate
2009-10-13	Cezary Kaliszyk	Regularizing HOL all.	file \| diff \| annotate
2009-10-13	Cezary Kaliszyk	":" is used for being in a set, "IN" means something else...	file \| diff \| annotate
2009-10-13	Cezary Kaliszyk	First (untested) version of regularize for abstractions.	file \| diff \| annotate
2009-10-12	Christian Urban	slightly modified the parser	file \| diff \| annotate

nominal2