paulson [Fri, 11 Jul 1997 13:28:53 +0200] rev 3514
Moved some declarations to Message from Public and Shared
paulson [Fri, 11 Jul 1997 13:27:15 +0200] rev 3513
Now loads theory Event, which contains common declarations
paulson [Fri, 11 Jul 1997 13:26:15 +0200] rev 3512
Moving common declarations and proofs from theories "Shared"
and "Public" to "Event". NB the original "Event" theory was later renamed "Shared".
Addition of the Notes constructor to datatype "event".
wenzelm [Wed, 09 Jul 1997 17:00:34 +0200] rev 3511
removed obsolete init_pps and init_thy_reader;
wenzelm [Wed, 09 Jul 1997 16:54:17 +0200] rev 3510
improved type checking errors;
wenzelm [Wed, 09 Jul 1997 16:53:53 +0200] rev 3509
removed init_pps;
wenzelm [Wed, 09 Jul 1997 16:52:51 +0200] rev 3508
removed init_database;
nipkow [Wed, 09 Jul 1997 12:57:04 +0200] rev 3507
Improved length = size translation.
paulson [Mon, 07 Jul 1997 10:49:14 +0200] rev 3506
New proofs involving CERTIFICATE VERIFY
wenzelm [Mon, 07 Jul 1997 09:09:21 +0200] rev 3505
eliminated chmod -w;
wenzelm [Mon, 07 Jul 1997 09:07:08 +0200] rev 3504
-w option;
wenzelm [Mon, 07 Jul 1997 09:06:26 +0200] rev 3503
NOWRITE;
wenzelm [Mon, 07 Jul 1997 09:05:16 +0200] rev 3502
added -w option;
paulson [Fri, 04 Jul 1997 17:36:41 +0200] rev 3501
Changed some variables of type msg to lower case (e.g. from NB to nb
paulson [Fri, 04 Jul 1997 17:34:55 +0200] rev 3500
New constant "certificate"--just an abbreviation
nipkow [Fri, 04 Jul 1997 14:37:30 +0200] rev 3499
Reduced priority of postfix ^* etc operators such that they are the same as
application. Eg wf r^* now needs to be written wf(r^*).
paulson [Fri, 04 Jul 1997 12:36:00 +0200] rev 3498
Automatic update
paulson [Fri, 04 Jul 1997 12:32:31 +0200] rev 3497
Now catches the error of calling tgoalw when there are no goals to prove,
instead of just letting USyntax.list_mk_conj raise an exception
paulson [Fri, 04 Jul 1997 12:31:20 +0200] rev 3496
Simplified the new proofs about division
paulson [Fri, 04 Jul 1997 11:57:33 +0200] rev 3495
New comments on how to deal with unproved termination conditions
paulson [Fri, 04 Jul 1997 11:56:49 +0200] rev 3494
Fixed comments
paulson [Fri, 04 Jul 1997 11:56:18 +0200] rev 3493
Moved MLWorks.ML to its proper place, directory ML-Systems.
Note that MLWorks does not quite work yet, especially top-level pretty
printing
paulson [Fri, 04 Jul 1997 11:54:43 +0200] rev 3492
Automatic update
paulson [Thu, 03 Jul 1997 17:21:14 +0200] rev 3491
Modified the \tydx command to set types in italics instead of \tt
paulson [Thu, 03 Jul 1997 17:20:07 +0200] rev 3490
Some LaTeX-2e primitives such as \texttt
A bit of material on theories Primes and Primrec
paulson [Thu, 03 Jul 1997 17:17:45 +0200] rev 3489
Added documentation for recdef, and tidied some other material
paulson [Thu, 03 Jul 1997 17:10:50 +0200] rev 3488
Updated references
nipkow [Thu, 03 Jul 1997 13:44:54 +0200] rev 3487
set_of_list -> set