Thu, 21 Sep 2006 19:05:01 +0200 tuned eta_contract;
wenzelm [Thu, 21 Sep 2006 19:05:01 +0200] rev 20670
tuned eta_contract;
Thu, 21 Sep 2006 19:04:55 +0200 added dest_equals_rhs;
wenzelm [Thu, 21 Sep 2006 19:04:55 +0200] rev 20669
added dest_equals_rhs; moved dest_binop to thm.ML;
Thu, 21 Sep 2006 19:04:49 +0200 tuned;
wenzelm [Thu, 21 Sep 2006 19:04:49 +0200] rev 20668
tuned;
Thu, 21 Sep 2006 19:04:43 +0200 serial numbers for consts;
wenzelm [Thu, 21 Sep 2006 19:04:43 +0200] rev 20667
serial numbers for consts; added serial_of/name_of;
Thu, 21 Sep 2006 19:04:36 +0200 Thm.dest_binop;
wenzelm [Thu, 21 Sep 2006 19:04:36 +0200] rev 20666
Thm.dest_binop;
Thu, 21 Sep 2006 19:04:29 +0200 member (op =);
wenzelm [Thu, 21 Sep 2006 19:04:29 +0200] rev 20665
member (op =); ThmDatabase.is_ml_reserved; tuned oracle name;
Thu, 21 Sep 2006 19:04:20 +0200 member (op =);
wenzelm [Thu, 21 Sep 2006 19:04:20 +0200] rev 20664
member (op =);
Thu, 21 Sep 2006 19:04:12 +0200 updated timings;
wenzelm [Thu, 21 Sep 2006 19:04:12 +0200] rev 20663
updated timings;
Thu, 21 Sep 2006 17:39:57 +0200 new function hashw_int
paulson [Thu, 21 Sep 2006 17:39:57 +0200] rev 20662
new function hashw_int
Thu, 21 Sep 2006 17:33:11 +0200 Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson [Thu, 21 Sep 2006 17:33:11 +0200] rev 20661
Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions unless theorems differ by sorts alone, which should not matter. Also minor fixes to standard hashing.
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip