Sat, 17 Dec 2011 15:09:11 +0100 eliminated Drule.export_without_context which is not really required here;
wenzelm [Sat, 17 Dec 2011 15:09:11 +0100] rev 45910
eliminated Drule.export_without_context which is not really required here;
Sat, 17 Dec 2011 13:08:03 +0100 tuned signature;
wenzelm [Sat, 17 Dec 2011 13:08:03 +0100] rev 45909
tuned signature;
Sat, 17 Dec 2011 12:51:30 +0100 enforce short hostname on all platforms (especially macbroy2);
wenzelm [Sat, 17 Dec 2011 12:51:30 +0100] rev 45908
enforce short hostname on all platforms (especially macbroy2);
Sat, 17 Dec 2011 12:42:10 +0100 clarified modules that contribute to datatype package;
wenzelm [Sat, 17 Dec 2011 12:42:10 +0100] rev 45907
clarified modules that contribute to datatype package;
Sat, 17 Dec 2011 12:10:37 +0100 tuned signature;
wenzelm [Sat, 17 Dec 2011 12:10:37 +0100] rev 45906
tuned signature;
Fri, 16 Dec 2011 22:07:03 +0100 merged
wenzelm [Fri, 16 Dec 2011 22:07:03 +0100] rev 45905
merged
Fri, 16 Dec 2011 12:01:10 +0100 merged
nipkow [Fri, 16 Dec 2011 12:01:10 +0100] rev 45904
merged
Fri, 16 Dec 2011 12:00:59 +0100 improved indexed complete lattice
nipkow [Fri, 16 Dec 2011 12:00:59 +0100] rev 45903
improved indexed complete lattice
Fri, 16 Dec 2011 22:08:48 +0100 more elementary defs;
wenzelm [Fri, 16 Dec 2011 22:08:48 +0100] rev 45902
more elementary defs;
Fri, 16 Dec 2011 21:23:21 +0100 eliminated old-fashioned Global_Theory.add_thms(s);
wenzelm [Fri, 16 Dec 2011 21:23:21 +0100] rev 45901
eliminated old-fashioned Global_Theory.add_thms(s);
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip