nominal2: File revisions

Quot/Examples/AbsRepTest.thy

Sat, 26 Dec 2009 21:36:20 +0100	Christian Urban	renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy	file \| diff \| annotate
Sat, 26 Dec 2009 07:15:30 +0100	Christian Urban	generalised absrep function; needs consolidation	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
Thu, 24 Dec 2009 00:58:50 +0100	Christian Urban	used Local_Theory.declaration for storing quotdata	file \| diff \| annotate
Wed, 23 Dec 2009 22:42:30 +0100	Christian Urban	modified mk_resp_arg so that the user can give terms as equivalence relations, not just constants	file \| diff \| annotate
Wed, 23 Dec 2009 13:23:33 +0100	Christian Urban	explicit handling of mem_def, avoiding the use of the simplifier; this fixes some quotient_type definitions	file \| diff \| annotate
Wed, 23 Dec 2009 10:31:54 +0100	Christian Urban	corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file	file \| diff \| annotate

nominal2