nominal2: File revisions

Quot/Examples/LamEx.thy

Wed, 20 Jan 2010 12:33:19 +0100	Cezary Kaliszyk	Statement of term1_hom_rsp	file \| diff \| annotate
Wed, 20 Jan 2010 12:20:18 +0100	Christian Urban	proved that the function is a function	file \| diff \| annotate
Wed, 20 Jan 2010 11:30:32 +0100	Cezary Kaliszyk	term1_hom as a function	file \| diff \| annotate
Tue, 19 Jan 2010 18:17:42 +0100	Cezary Kaliszyk	A version of hom with quantifiers.	file \| diff \| annotate
Sat, 16 Jan 2010 04:23:27 +0100	Christian Urban	fixed broken (partial) proof	file \| diff \| annotate
Sat, 16 Jan 2010 03:56:00 +0100	Christian Urban	used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on	file \| diff \| annotate
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

nominal2