nominal2: File revisions

Quot/Examples/FSet2.thy

Thu, 24 Dec 2009 22:28:19 +0100	Christian Urban	made the quotient_type definition more like typedef; now type variables need to be explicitly given	file \| diff \| annotate
Mon, 21 Dec 2009 22:36:31 +0100	Christian Urban	get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO	file \| diff \| annotate
Sun, 20 Dec 2009 00:53:35 +0100	Christian Urban	on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file	file \| diff \| annotate
Sun, 20 Dec 2009 00:26:53 +0100	Christian Urban	renamed "quotient" command to "quotient_type"; needs new keyword file to be installed	file \| diff \| annotate
Fri, 11 Dec 2009 11:08:58 +0100	Cezary Kaliszyk	New syntax for definitions.	file \| diff \| annotate
Thu, 10 Dec 2009 03:48:39 +0100	Christian Urban	added an attempt to get a finite set theory	file \| diff \| annotate

nominal2