nominal2: File revisions

Nominal/NewParser.thy

Mon, 03 May 2010 12:24:27 +0200	Cezary Kaliszyk	Introduce eq_iff_simp to match the one from Parser.	file \| diff \| annotate
Mon, 03 May 2010 11:43:08 +0200	Cezary Kaliszyk	Cheat support equations in new parser	file \| diff \| annotate
Mon, 03 May 2010 10:15:23 +0200	Cezary Kaliszyk	Add explicit cheats in NewParser and comment out the examples for outside use.	file \| diff \| annotate
Mon, 03 May 2010 09:57:05 +0200	Cezary Kaliszyk	Fix Datatype_Aux calls in NewParser.	file \| diff \| annotate
Sun, 02 May 2010 16:02:27 +0100	Christian Urban	tried to add some comments in the huge(!) nominal2_cmd function	file \| diff \| annotate
Sun, 02 May 2010 14:06:26 +0100	Christian Urban	attempted to remove dependency on (old) Fv and (old) Parser; lifting still uses Fv.thy; the examples do not work at the moment (with equivp proofs failing)	file \| diff \| annotate
Sat, 01 May 2010 09:15:46 +0100	Christian Urban	merged	file \| diff \| annotate
Sat, 01 May 2010 09:14:25 +0100	Christian Urban	tuned	file \| diff \| annotate

nominal2