Fri, 16 Dec 2011 12:03:33 +0100prefer Name.context operations;
wenzelm [Fri, 16 Dec 2011 12:03:33 +0100] rev 46772
prefer Name.context operations;

Fri, 16 Dec 2011 12:01:10 +0100merged
nipkow [Fri, 16 Dec 2011 12:01:10 +0100] rev 46771
merged

Fri, 16 Dec 2011 12:00:59 +0100improved indexed complete lattice
nipkow [Fri, 16 Dec 2011 12:00:59 +0100] rev 46770
improved indexed complete lattice

Fri, 16 Dec 2011 11:02:55 +0100tuned;
wenzelm [Fri, 16 Dec 2011 11:02:55 +0100] rev 46769
tuned;

Fri, 16 Dec 2011 10:52:35 +0100clarified modules that contribute to datatype package;
wenzelm [Fri, 16 Dec 2011 10:52:35 +0100] rev 46768
clarified modules that contribute to datatype package;

Fri, 16 Dec 2011 10:38:38 +0100tuned signature;
wenzelm [Fri, 16 Dec 2011 10:38:38 +0100] rev 46767
tuned signature;

Thu, 15 Dec 2011 21:46:52 +0100merged;
wenzelm [Thu, 15 Dec 2011 21:46:52 +0100] rev 46766
merged;

Thu, 15 Dec 2011 19:53:28 +0100tuned;
wenzelm [Thu, 15 Dec 2011 19:53:28 +0100] rev 46765
tuned;

Thu, 15 Dec 2011 18:08:40 +0100clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
wenzelm [Thu, 15 Dec 2011 18:08:40 +0100] rev 46764
clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;

Thu, 15 Dec 2011 17:37:14 +0100separate rep_datatype.ML;
wenzelm [Thu, 15 Dec 2011 17:37:14 +0100] rev 46763
separate rep_datatype.ML;
tuned signature;