1997-07-09 wenzelm 1997-07-09 improved type checking errors;
1997-07-09 wenzelm 1997-07-09 removed init_pps;
1997-07-09 wenzelm 1997-07-09 removed init_database;
1997-07-09 nipkow 1997-07-09 Improved length = size translation.
1997-07-07 paulson 1997-07-07 New proofs involving CERTIFICATE VERIFY
1997-07-07 wenzelm 1997-07-07 eliminated chmod -w;
1997-07-07 wenzelm 1997-07-07 -w option;
1997-07-07 wenzelm 1997-07-07 NOWRITE;
1997-07-07 wenzelm 1997-07-07 added -w option;
1997-07-04 paulson 1997-07-04 Changed some variables of type msg to lower case (e.g. from NB to nb
1997-07-04 paulson 1997-07-04 New constant "certificate"--just an abbreviation
1997-07-04 nipkow 1997-07-04 Reduced priority of postfix ^* etc operators such that they are the same as application. Eg wf r^* now needs to be written wf(r^*).
1997-07-04 paulson 1997-07-04 Automatic update
1997-07-04 paulson 1997-07-04 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
1997-07-04 paulson 1997-07-04 Simplified the new proofs about division
1997-07-04 paulson 1997-07-04 New comments on how to deal with unproved termination conditions
1997-07-04 paulson 1997-07-04 Fixed comments
1997-07-04 paulson 1997-07-04 Moved MLWorks.ML to its proper place, directory ML-Systems. Note that MLWorks does not quite work yet, especially top-level pretty printing
1997-07-04 paulson 1997-07-04 Automatic update
1997-07-03 paulson 1997-07-03 Modified the \tydx command to set types in italics instead of \tt
1997-07-03 paulson 1997-07-03 Some LaTeX-2e primitives such as \texttt A bit of material on theories Primes and Primrec
1997-07-03 paulson 1997-07-03 Added documentation for recdef, and tidied some other material
1997-07-03 paulson 1997-07-03 Updated references
1997-07-03 nipkow 1997-07-03 set_of_list -> set
1997-07-02 paulson 1997-07-02 Now there are TWO spaces after each full stop, so that the Emacs sentence primitives work
1997-07-02 paulson 1997-07-02 Now there are TWO spaces after each full stop, so that the Emacs sentence primitives work
1997-07-02 nipkow 1997-07-02 Added the following lemmas tp Divides and a few others to Arith and NatDef: div_le_mono, div_le_mono2, div_le_dividend, div_less_dividend Fixed a broken proof in WF_Rel.ML. No idea what caused this.
1997-07-01 paulson 1997-07-01 Tidying; also simplified the lemma Says_Server_not
1997-07-01 paulson 1997-07-01 New theory TLS
1997-07-01 paulson 1997-07-01 Deleted a redundant A~=B in rules that refer to a previous event
1997-07-01 paulson 1997-07-01 More realistic model: the Spy can compute clientK and serverK
1997-07-01 paulson 1997-07-01 Reordered rules in analz_image_freshK_ss to improve clarity
1997-07-01 paulson 1997-07-01 Removal of the obsolete newN function
1997-07-01 paulson 1997-07-01 New theorem priK_inj_eq, injectivity of priK
1997-07-01 paulson 1997-07-01 spy_analz_tac: Restored iffI to the list of rules used to break down the subgoal
1997-07-01 paulson 1997-07-01 New theory TLS
1997-07-01 paulson 1997-07-01 Baby TLS. Proofs work, but model seems unrealistic
1997-07-01 paulson 1997-07-01 New and stronger lemmas; more default simp/cla rules
1997-07-01 paulson 1997-07-01 Deleted the obsolete operators newK, newN and nPair
1997-07-01 paulson 1997-07-01 Now the possibility proof calls the appropriate tactic
1997-07-01 paulson 1997-07-01 Added a comment
1997-07-01 paulson 1997-07-01 Now Collect_mem_eq is a default simprule (how could it have ever been omitted?
1997-07-01 paulson 1997-07-01 New laws for the "lists" operator
1997-06-30 nipkow 1997-06-30 More concat lemmas.
1997-06-27 paulson 1997-06-27 Corrected indentations and margins after the renaming of "set_of_list"
1997-06-26 nipkow 1997-06-26 set_of_list -> set
1997-06-26 paulson 1997-06-26 Trivial changes in connection with the Yahalom paper. Changed the order of the premises in no_nonce_YM1_YM2. Installed B_trusts_YM4_newK using bind_thm. Improved some comments.
1997-06-26 wenzelm 1997-06-26 oops;
1997-06-26 wenzelm 1997-06-26 rearrange pages of ps file to be printed as booklet (duplex);
1997-06-26 nipkow 1997-06-26 amdI -> admI2
1997-06-26 nipkow 1997-06-26 Tuned Franz's proofs.
1997-06-23 paulson 1997-06-23 Removal of structure Context and its replacement by a theorem list of congruence rules for use in CONTEXT_REWRITE_RULE (where definitions are processed)
1997-06-23 paulson 1997-06-23 Removal of COND_CONG, which is just if_cong RS eq_reflection
1997-06-23 paulson 1997-06-23 Ran expandshort
1997-06-23 paulson 1997-06-23 New "congs" keyword for recdef theory section
1997-06-20 wenzelm 1997-06-20 removed old Makefile;
1997-06-20 wenzelm 1997-06-20 removed;
1997-06-20 wenzelm 1997-06-20 removed old Makefile;
1997-06-20 wenzelm 1997-06-20 removed old Makefile and compat files;
1997-06-19 paulson 1997-06-19 Made proofs more concise by replacing calls to spy_analz_tac by uses of analz_insert_eq in rewriting