nominal2: File revisions

Nominal/Ex/Lambda.thy

2011-08-19	Cezary Kaliszyk	Comment out examples with 'True' that do not work because function still does not work	file \| diff \| annotate
2011-07-22	Christian Urban	completed the eqvt-proofs for functions; they are stored under the name function_name.eqvt and added to the eqvt-list	file \| diff \| annotate
2011-07-19	Christian Urban	preliminary version of automatically generation the eqvt-lemmas for functions defined with nominal_primrec	file \| diff \| annotate
2011-07-19	Christian Urban	generated the partial eqvt-theorem for functions	file \| diff \| annotate
2011-07-18	Christian Urban	added a flag (eqvt) to termination proofs arising fron nominal_primrecs	file \| diff \| annotate
2011-07-18	Christian Urban	moved eqvt for Option.map	file \| diff \| annotate
2011-07-05	Christian Urban	added some relatively simple examples from paper by Norrish	file \| diff \| annotate
2011-07-05	Christian Urban	changed bind to binds in specifications; bind will cause trouble with Monad_Syntax	file \| diff \| annotate
2011-07-05	Christian Urban	made the tests go through again	file \| diff \| annotate
2011-07-05	Christian Urban	merged	file \| diff \| annotate
2011-07-05	Christian Urban	exported various FCB-lemmas to a separate file	file \| diff \| annotate
2011-07-05	Cezary Kaliszyk	Express trans_db with Option.map and Option.bind. Possibly mbind is a copy of bind?	file \| diff \| annotate

nominal2