nominal2: File revisions

LFex.thy

2009-12-06	Christian Urban	fixed examples	file \| diff \| annotate
2009-12-06	Christian Urban	merged	file \| diff \| annotate
2009-12-06	Christian Urban	added a theorem list for equivalence theorems	file \| diff \| annotate
2009-12-06	Cezary Kaliszyk	Name changes.	file \| diff \| annotate
2009-12-06	Cezary Kaliszyk	Simpler definition code that works with any type maps.	file \| diff \| annotate
2009-12-05	Cezary Kaliszyk	Definitions folded first.	file \| diff \| annotate
2009-12-05	Christian Urban	simplified inj_repabs_trm	file \| diff \| annotate
2009-12-04	Cezary Kaliszyk	more name cleaning and removing	file \| diff \| annotate
2009-12-04	Cezary Kaliszyk	merged	file \| diff \| annotate
2009-12-04	Christian Urban	merge	file \| diff \| annotate
2009-12-04	Cezary Kaliszyk	Removed previous inj_repabs_tac	file \| diff \| annotate
2009-12-04	Cezary Kaliszyk	rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.	file \| diff \| annotate
2009-12-04	Cezary Kaliszyk	Using APPLY_RSP1; again a little bit faster.	file \| diff \| annotate
2009-12-04	Cezary Kaliszyk	The big merge; probably non-functional.	file \| diff \| annotate
2009-12-04	Cezary Kaliszyk	Testing the new tactic everywhere	file \| diff \| annotate

nominal2