| 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 |
| Tue, 18 Dec 2007 19:15:31 +0100 | huffman | rearrange into subsections | changeset | files |
| Tue, 18 Dec 2007 18:39:00 +0100 | paulson | Skolemization now catches exception THM, which may be raised if unification fails. | changeset | files |
| Tue, 18 Dec 2007 17:37:25 +0100 | paulson | Deleted redundant setmp calls | changeset | files |
| Tue, 18 Dec 2007 16:26:46 +0100 | wenzelm | tuned proofs, document; | changeset | files |