isabelle: File revisions

src/HOL/Nominal/nominal_thmdecls.ML

Mon, 07 May 2007 00:49:59 +0200	wenzelm	simplified DataFun interfaces;	file \| diff \| annotate
Mon, 16 Apr 2007 07:32:23 +0200	urbanc	improved the equivariance lemmas for the quantifiers; had to export the lemma eqvt_force_add and eqvt_force_del in the thmdecls	file \| diff \| annotate
Mon, 02 Apr 2007 23:24:52 +0200	narboux	rename bij and fresh into bijs and freshs and lookup for eqvts lemma using the ml value instead of the name	file \| diff \| annotate
Wed, 28 Mar 2007 18:25:23 +0200	urbanc	the name for the collection of equivariance lemmas is now eqvts (changed from eqvt) in order to avoid clashes with eqvt-lemmas generated in nominal_inductive	file \| diff \| annotate
Thu, 22 Mar 2007 11:17:32 +0100	urbanc	clarified an error-message	file \| diff \| annotate
Mon, 12 Mar 2007 16:25:39 +0100	narboux	removes some unused code that used to try to derive a simpler version of the eqvt lemmas	file \| diff \| annotate
Tue, 06 Mar 2007 15:28:22 +0100	urbanc	major update of the nominal package; there is now an infrastructure	file \| diff \| annotate
Thu, 08 Feb 2007 17:22:22 +0100	urbanc	added get-functions	file \| diff \| annotate
Tue, 06 Feb 2007 15:12:18 +0100	urbanc	fixed two stupid bugs of SML to do with the value restriction and missing type	file \| diff \| annotate
Tue, 06 Feb 2007 00:41:54 +0100	urbanc	moved the infrastructure from the nominal_tags file to nominal_thmdecls	file \| diff \| annotate

isabelle