Thu, 20 Dec 2007 13:58:45 +0100 wenzelm adapted theory name;
Thu, 20 Dec 2007 13:31:30 +0100 wenzelm * Metis prover an order of magnitude faster, works with multithreading.
Thu, 20 Dec 2007 12:02:46 +0100 wenzelm updated HOL-Nominal-Examples deps;
Thu, 20 Dec 2007 11:16:19 +0100 wenzelm made refute non-critical (seems to work after avoiding floating point random numbers);
Thu, 20 Dec 2007 03:06:20 +0100 huffman move bottom-related stuff back into Pcpo.thy
Thu, 20 Dec 2007 01:07:21 +0100 urbanc polishing of some proofs
Thu, 20 Dec 2007 00:19:40 +0100 wenzelm Random.range_real makes SML/NJ happy;
Wed, 19 Dec 2007 23:49:28 +0100 wenzelm tuned comments;
Wed, 19 Dec 2007 23:42:20 +0100 wenzelm tuned RandomWord signature;
Wed, 19 Dec 2007 23:10:17 +0100 wenzelm removed strange MacRoman character;
Wed, 19 Dec 2007 23:06:16 +0100 wenzelm using RandomWord from Isabelle/Pure gains factor 10-20 speedup;
Wed, 19 Dec 2007 23:06:16 +0100 wenzelm updated;
Wed, 19 Dec 2007 23:06:14 +0100 wenzelm added General/random_word.ML;
Wed, 19 Dec 2007 23:06:14 +0100 wenzelm Simple generator for pseudo-random numbers, using unboxed word arithmetic only.
Wed, 19 Dec 2007 23:06:13 +0100 wenzelm removed duplicate CRITICAL markup;
Wed, 19 Dec 2007 22:34:03 +0100 haftmann instantiation target
Wed, 19 Dec 2007 22:33:44 +0100 haftmann tuned primitive inferences
Wed, 19 Dec 2007 17:40:48 +0100 paulson Replaced refs by config params; finer critical section in mets method
Wed, 19 Dec 2007 16:52:26 +0100 wenzelm simultaneous use_thys;
Wed, 19 Dec 2007 16:52:07 +0100 wenzelm marked refute (the main metis procedure) as CRITICAL;
Wed, 19 Dec 2007 16:32:16 +0100 schirmer more examples
Wed, 19 Dec 2007 16:32:14 +0100 schirmer accomodate to replacement of K_record by %x.c
Wed, 19 Dec 2007 16:32:12 +0100 schirmer replaced K_record by lambda term %x. c
Tue, 18 Dec 2007 22:21:42 +0100 wenzelm signature BASIC_MULTITHREADING;
Tue, 18 Dec 2007 22:21:41 +0100 wenzelm removed obsolete use_noncritical (plain use is already non-critical);
Tue, 18 Dec 2007 22:21:40 +0100 wenzelm serial: now based on specific version in structure Multithreading;
Tue, 18 Dec 2007 22:18:31 +0100 huffman add class ppo of pointed partial orders;
Tue, 18 Dec 2007 19:54:34 +0100 wenzelm named some critical sections;
Tue, 18 Dec 2007 19:54:33 +0100 wenzelm named some critical sections;
Tue, 18 Dec 2007 19:54:32 +0100 wenzelm use_text/use_file: non-critical (Poly/ML compiler is thread-safe);
Tue, 18 Dec 2007 19:54:31 +0100 wenzelm non-critical (accidental concurrent access does not affect functional integrity);
Tue, 18 Dec 2007 19:54:30 +0100 wenzelm PrintMode.setmp (avoid direct access to print_mode ref);
Tue, 18 Dec 2007 19:15:31 +0100 huffman rearrange into subsections
Tue, 18 Dec 2007 18:39:00 +0100 paulson Skolemization now catches exception THM, which may be raised if unification fails.
Tue, 18 Dec 2007 17:37:25 +0100 paulson Deleted redundant setmp calls
Tue, 18 Dec 2007 16:26:46 +0100 wenzelm tuned proofs, document;
Tue, 18 Dec 2007 14:37:00 +0100 haftmann switched from PreList to ATP_Linkup
Tue, 18 Dec 2007 12:26:24 +0100 berghofe Renamed *.size to prod.size.
Tue, 18 Dec 2007 12:26:00 +0100 berghofe Alternative names are now also used when storing theorems for
Tue, 18 Dec 2007 11:45:08 +0100 krauss temporarily fixed documentation due to changed size functions
Tue, 18 Dec 2007 00:17:00 +0100 wenzelm split_primel: salvaged original proof after blow with sledghammer
Mon, 17 Dec 2007 23:33:00 +0100 wenzelm cond_timeit: added message argument, use Exn.capture/release;
Mon, 17 Dec 2007 23:26:27 +0100 wenzelm cond_timeit: added message argument;
Mon, 17 Dec 2007 22:40:14 +0100 haftmann note in target
Mon, 17 Dec 2007 22:40:13 +0100 haftmann maior tuning
Mon, 17 Dec 2007 22:40:12 +0100 haftmann tuned
Mon, 17 Dec 2007 18:39:18 +0100 berghofe Added foldl1.
Mon, 17 Dec 2007 18:38:28 +0100 berghofe Adapted to changes in size function.
Mon, 17 Dec 2007 18:37:49 +0100 berghofe size functions for nested datatypes are now expressed using
Mon, 17 Dec 2007 18:32:56 +0100 berghofe Adapted to changes in interface of indtac.
Mon, 17 Dec 2007 18:31:52 +0100 berghofe - Removed redundant head_len field in datatype_info
Mon, 17 Dec 2007 18:30:44 +0100 berghofe - Removed redundant head_len field in datatype_info
Mon, 17 Dec 2007 18:27:48 +0100 paulson tidied some messy proofs
Mon, 17 Dec 2007 18:24:44 +0100 berghofe Deleted copy of indtac.
Mon, 17 Dec 2007 18:23:50 +0100 berghofe Added code lemma for message_string_size.
Mon, 17 Dec 2007 18:22:48 +0100 berghofe Removed obsolete lemma size_sum.
Mon, 17 Dec 2007 18:11:21 +0100 paulson fixed ancestors
Mon, 17 Dec 2007 18:01:51 +0100 haftmann whitespace typo
Mon, 17 Dec 2007 17:57:52 +0100 haftmann explicit closing of derived witnesses
Mon, 17 Dec 2007 17:57:51 +0100 haftmann closed rules
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip