nominal2: File revisions

Quot/Examples/LamEx.thy

Sat, 16 Jan 2010 02:09:38 +0100	Christian Urban	liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals	file \| diff \| annotate
Fri, 15 Jan 2010 17:09:36 +0100	Christian Urban	added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions	file \| diff \| annotate
Fri, 15 Jan 2010 16:13:49 +0100	Christian Urban	tried to witness the hom-lemma with the recursion combinator from rlam....does not work yet completely	file \| diff \| annotate
Fri, 15 Jan 2010 15:51:25 +0100	Cezary Kaliszyk	hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.	file \| diff \| annotate
Fri, 15 Jan 2010 12:17:30 +0100	Christian Urban	slight tuning of relation_error	file \| diff \| annotate
Fri, 15 Jan 2010 11:04:21 +0100	Cezary Kaliszyk	Appropriate respects and a statement of the lifted hom lemma	file \| diff \| annotate

nominal2