nominal2: File revisions

Nominal/nominal_function.ML

Sun, 28 Aug 2011 14:50:13 +0100	Christian Urban	updated to Isabelle 28 Aug	file \| diff \| annotate
Wed, 17 Aug 2011 22:56:07 +0200	Christian Urban	made same changes as in main branch	file \| diff \| annotate
Mon, 15 Aug 2011 17:42:35 +0200	Christian Urban	uodated to new Isabelle (15. Aug)	file \| diff \| annotate
Tue, 19 Jul 2011 01:40:36 +0100	Christian Urban	generated the partial eqvt-theorem for functions	file \| diff \| annotate
Mon, 18 Jul 2011 17:40:13 +0100	Christian Urban	added a flag (eqvt) to termination proofs arising fron nominal_primrecs	file \| diff \| annotate
Thu, 16 Jun 2011 13:14:16 +0100	Christian Urban	added eqvt_at and invariant for boths sides of the equations	file \| diff \| annotate
Thu, 16 Jun 2011 12:12:25 +0100	Christian Urban	added a test that every function must be of pt-sort	file \| diff \| annotate
Tue, 07 Jun 2011 08:52:59 +0100	Christian Urban	fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant	file \| diff \| annotate

nominal2