2007-12-20 ago wenzelm added get/put_data;
2007-12-20 ago wenzelm separated into global template vs. thread-local value;
2007-12-20 ago wenzelm Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
2007-12-20 ago wenzelm added ML-Systems/universal.ML;
2007-12-20 ago wenzelm updated;
2007-12-20 ago wenzelm obsolete;
2007-12-20 ago wenzelm removed obsolete (slow!) Random implementation;
2007-12-20 ago wenzelm moved Pure/General/random_word.ML to Tools/random_word.ML;
2007-12-20 ago wenzelm adapted theory name;
2007-12-20 ago wenzelm * Metis prover an order of magnitude faster, works with multithreading.
2007-12-20 ago wenzelm updated HOL-Nominal-Examples deps;
2007-12-20 ago wenzelm made refute non-critical (seems to work after avoiding floating point random numbers);
2007-12-20 ago huffman move bottom-related stuff back into Pcpo.thy
2007-12-20 ago urbanc polishing of some proofs
2007-12-20 ago wenzelm Random.range_real makes SML/NJ happy;
2007-12-19 ago wenzelm tuned comments;
2007-12-19 ago wenzelm tuned RandomWord signature;
2007-12-19 ago wenzelm removed strange MacRoman character;
2007-12-19 ago wenzelm using RandomWord from Isabelle/Pure gains factor 10-20 speedup;
2007-12-19 ago wenzelm updated;
2007-12-19 ago wenzelm added General/random_word.ML;
2007-12-19 ago wenzelm Simple generator for pseudo-random numbers, using unboxed word arithmetic only.
2007-12-19 ago wenzelm removed duplicate CRITICAL markup;
2007-12-19 ago haftmann instantiation target
2007-12-19 ago haftmann tuned primitive inferences
2007-12-19 ago paulson Replaced refs by config params; finer critical section in mets method
2007-12-19 ago wenzelm simultaneous use_thys;
2007-12-19 ago wenzelm marked refute (the main metis procedure) as CRITICAL;
2007-12-19 ago schirmer more examples
2007-12-19 ago schirmer accomodate to replacement of K_record by %x.c
2007-12-19 ago schirmer replaced K_record by lambda term %x. c
2007-12-18 ago wenzelm signature BASIC_MULTITHREADING;
2007-12-18 ago wenzelm removed obsolete use_noncritical (plain use is already non-critical);
2007-12-18 ago wenzelm serial: now based on specific version in structure Multithreading;
2007-12-18 ago huffman add class ppo of pointed partial orders;
2007-12-18 ago wenzelm named some critical sections;
2007-12-18 ago wenzelm named some critical sections;
2007-12-18 ago wenzelm use_text/use_file: non-critical (Poly/ML compiler is thread-safe);
2007-12-18 ago wenzelm non-critical (accidental concurrent access does not affect functional integrity);
2007-12-18 ago wenzelm PrintMode.setmp (avoid direct access to print_mode ref);
2007-12-18 ago huffman rearrange into subsections
2007-12-18 ago paulson Skolemization now catches exception THM, which may be raised if unification fails.
2007-12-18 ago paulson Deleted redundant setmp calls
2007-12-18 ago wenzelm tuned proofs, document;
2007-12-18 ago haftmann switched from PreList to ATP_Linkup
2007-12-18 ago berghofe Renamed *.size to prod.size.
2007-12-18 ago berghofe Alternative names are now also used when storing theorems for
2007-12-18 ago krauss temporarily fixed documentation due to changed size functions
2007-12-18 ago wenzelm split_primel: salvaged original proof after blow with sledghammer
2007-12-17 ago wenzelm cond_timeit: added message argument, use Exn.capture/release;
2007-12-17 ago wenzelm cond_timeit: added message argument;
2007-12-17 ago haftmann note in target
2007-12-17 ago haftmann maior tuning
2007-12-17 ago haftmann tuned
2007-12-17 ago berghofe Added foldl1.
2007-12-17 ago berghofe Adapted to changes in size function.
2007-12-17 ago berghofe size functions for nested datatypes are now expressed using
2007-12-17 ago berghofe Adapted to changes in interface of indtac.
2007-12-17 ago berghofe - Removed redundant head_len field in datatype_info
2007-12-17 ago berghofe - Removed redundant head_len field in datatype_info