nominal2: File revisions

Nominal/Nominal2.thy

2010-12-14	Christian Urban	freshness theorem in strong exhausts; (temporarily includes a cheat_tac to make all tests go through)	file \| diff \| annotate
2010-12-12	Christian Urban	created strong_exhausts terms	file \| diff \| annotate
2010-12-12	Christian Urban	moved setify and listify functions into the library; introduced versions that have a type argument	file \| diff \| annotate
2010-12-08	Christian Urban	first tests about exhaust	file \| diff \| annotate
2010-12-08	Christian Urban	moved some code into the nominal_library	file \| diff \| annotate
2010-12-08	Christian Urban	moved definition of raw bn-functions into nominal_dt_rawfuns	file \| diff \| annotate
2010-12-08	Christian Urban	kept the nested structure of constructors (belonging to one datatype)	file \| diff \| annotate
2010-12-07	Christian Urban	automated permute_bn theorems	file \| diff \| annotate
2010-12-06	Christian Urban	moved code from nominal_dt_supp to nominal_dt_quot	file \| diff \| annotate
2010-12-06	Christian Urban	automated alpha_perm_bn theorems	file \| diff \| annotate
2010-12-06	Christian Urban	ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof	file \| diff \| annotate
2010-11-15	Christian Urban	proved that bn functions return a finite set	file \| diff \| annotate

nominal2