nominal2: File revisions

Quot/Examples/FSet3.thy

Sat, 26 Dec 2009 20:45:37 +0100	Christian Urban	added an item about when the same quotient constant is defined twice (throws a bind exception in quoteint_def.ML)	file \| diff \| annotate
Sat, 26 Dec 2009 20:24:53 +0100	Christian Urban	as expected problems occure when lifting concat lemmas	file \| diff \| annotate
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
Wed, 23 Dec 2009 23:22:02 +0100	Christian Urban	renamed some fields in the info records	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

nominal2