| Thu, 20 Dec 2007 13:58:45 +0100 |
wenzelm |
adapted theory name;
|
changeset |
files
|
| Thu, 20 Dec 2007 13:31:30 +0100 |
wenzelm |
* Metis prover an order of magnitude faster, works with multithreading.
|
changeset |
files
|
| Thu, 20 Dec 2007 12:02:46 +0100 |
wenzelm |
updated HOL-Nominal-Examples deps;
|
changeset |
files
|
| Thu, 20 Dec 2007 11:16:19 +0100 |
wenzelm |
made refute non-critical (seems to work after avoiding floating point random numbers);
|
changeset |
files
|
| Thu, 20 Dec 2007 03:06:20 +0100 |
huffman |
move bottom-related stuff back into Pcpo.thy
|
changeset |
files
|
| Thu, 20 Dec 2007 01:07:21 +0100 |
urbanc |
polishing of some proofs
|
changeset |
files
|
| Thu, 20 Dec 2007 00:19:40 +0100 |
wenzelm |
Random.range_real makes SML/NJ happy;
|
changeset |
files
|
| Wed, 19 Dec 2007 23:49:28 +0100 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Wed, 19 Dec 2007 23:42:20 +0100 |
wenzelm |
tuned RandomWord signature;
|
changeset |
files
|
| Wed, 19 Dec 2007 23:10:17 +0100 |
wenzelm |
removed strange MacRoman character;
|
changeset |
files
|
| Wed, 19 Dec 2007 23:06:16 +0100 |
wenzelm |
using RandomWord from Isabelle/Pure gains factor 10-20 speedup;
|
changeset |
files
|
| Wed, 19 Dec 2007 23:06:16 +0100 |
wenzelm |
updated;
|
changeset |
files
|
| Wed, 19 Dec 2007 23:06:14 +0100 |
wenzelm |
added General/random_word.ML;
|
changeset |
files
|
| Wed, 19 Dec 2007 23:06:14 +0100 |
wenzelm |
Simple generator for pseudo-random numbers, using unboxed word arithmetic only.
|
changeset |
files
|
| Wed, 19 Dec 2007 23:06:13 +0100 |
wenzelm |
removed duplicate CRITICAL markup;
|
changeset |
files
|
| Wed, 19 Dec 2007 22:34:03 +0100 |
haftmann |
instantiation target
|
changeset |
files
|
| Wed, 19 Dec 2007 22:33:44 +0100 |
haftmann |
tuned primitive inferences
|
changeset |
files
|
| Wed, 19 Dec 2007 17:40:48 +0100 |
paulson |
Replaced refs by config params; finer critical section in mets method
|
changeset |
files
|
| Wed, 19 Dec 2007 16:52:26 +0100 |
wenzelm |
simultaneous use_thys;
|
changeset |
files
|
| Wed, 19 Dec 2007 16:52:07 +0100 |
wenzelm |
marked refute (the main metis procedure) as CRITICAL;
|
changeset |
files
|
| Wed, 19 Dec 2007 16:32:16 +0100 |
schirmer |
more examples
|
changeset |
files
|
| Wed, 19 Dec 2007 16:32:14 +0100 |
schirmer |
accomodate to replacement of K_record by %x.c
|
changeset |
files
|
| Wed, 19 Dec 2007 16:32:12 +0100 |
schirmer |
replaced K_record by lambda term %x. c
|
changeset |
files
|
| Tue, 18 Dec 2007 22:21:42 +0100 |
wenzelm |
signature BASIC_MULTITHREADING;
|
changeset |
files
|
| Tue, 18 Dec 2007 22:21:41 +0100 |
wenzelm |
removed obsolete use_noncritical (plain use is already non-critical);
|
changeset |
files
|
| Tue, 18 Dec 2007 22:21:40 +0100 |
wenzelm |
serial: now based on specific version in structure Multithreading;
|
changeset |
files
|
| Tue, 18 Dec 2007 22:18:31 +0100 |
huffman |
add class ppo of pointed partial orders;
|
changeset |
files
|
| Tue, 18 Dec 2007 19:54:34 +0100 |
wenzelm |
named some critical sections;
|
changeset |
files
|
| Tue, 18 Dec 2007 19:54:33 +0100 |
wenzelm |
named some critical sections;
|
changeset |
files
|
| Tue, 18 Dec 2007 19:54:32 +0100 |
wenzelm |
use_text/use_file: non-critical (Poly/ML compiler is thread-safe);
|
changeset |
files
|
| Tue, 18 Dec 2007 19:54:31 +0100 |
wenzelm |
non-critical (accidental concurrent access does not affect functional integrity);
|
changeset |
files
|
| Tue, 18 Dec 2007 19:54:30 +0100 |
wenzelm |
PrintMode.setmp (avoid direct access to print_mode ref);
|
changeset |
files
|