1996-09-25 paulson 1996-09-25 Prevention of Overflow exception (for SML/NJ) in gensym
1996-09-25 paulson 1996-09-25 Rationalized the rewriting of membership for {} and insert by deleting the redundant theorems in_empty and in_insert
1996-09-25 paulson 1996-09-25 Calls discgarb -c to realize dramatic space savings!
1996-09-24 paulson 1996-09-24 Fixed spelling error in comment
1996-09-24 paulson 1996-09-24 Added miniscoping for UN and INT
1996-09-24 paulson 1996-09-24 Restoration of reference to Nipkow, LICS, 1993
1996-09-24 nipkow 1996-09-24 Moved Option out of IOA into core HOL
1996-09-24 nipkow 1996-09-24 Moved Option into core HOL which caused a few local changes.
1996-09-23 paulson 1996-09-23 Proofs made more robust to work in presence of le_refl
1996-09-23 paulson 1996-09-23 Now uses init_html
1996-09-23 paulson 1996-09-23 Simplification of proof of unique_session_keys
1996-09-23 paulson 1996-09-23 Correction of protocol; addition of Reveal message; proofs of correctness in its presence
1996-09-23 paulson 1996-09-23 Proof of Says_imp_old_keys is now more robust
1996-09-23 paulson 1996-09-23 Removal of the Notes constructor
1996-09-23 paulson 1996-09-23 New laws for messages
1996-09-23 paulson 1996-09-23 Simplification of definition of synth
1996-09-23 paulson 1996-09-23 Addition of le_refl to default simpset/claset
1996-09-23 paulson 1996-09-23 Removal of reference Nipkow-LICS-93
1996-09-23 paulson 1996-09-23 Proof of mult_le_mono is now more robust
1996-09-23 paulson 1996-09-23 New infix syntax: breaks line BEFORE operator
1996-09-23 paulson 1996-09-23 Optimized version of SELECT_GOAL, up to 10% faster
1996-09-23 paulson 1996-09-23 New operations on cterms. Now same names as in Logic
1996-09-23 paulson 1996-09-23 Addition of gensym
1996-09-23 paulson 1996-09-23 Bad version of Otway-Rees and the new attack on it
1996-09-13 paulson 1996-09-13 Reformatting; proved B_gets_secure_key
1996-09-13 paulson 1996-09-13 Abstraction of enemy_analz_tac over its argument
1996-09-13 paulson 1996-09-13 Reformatting
1996-09-13 paulson 1996-09-13 Reordering of premises for cut theorems, and new law MPair_synth_analz
1996-09-13 paulson 1996-09-13 No longer assumes Alice is not the Enemy in NS3. Proofs do not need it, and the assumption complicated the liveness argument
1996-09-13 paulson 1996-09-13 Uses the improved enemy_analz_tac of Shared.ML, with simpler proofs Weak liveness
1996-09-13 paulson 1996-09-13 Addition of Yahalom protocol
1996-09-13 paulson 1996-09-13 Removal of obsolete thm Fake_parts_insert
1996-09-13 paulson 1996-09-13 Addition of enemy_analz_tac and safe_solver Use of AddIffs for theorems about keys
1996-09-12 oheimb 1996-09-12 added flat_eq, renamed adm_disj_lemma11 to adm_lemma11, localized adm_disj_lemma1, ..., adm_disj_lemma10, adm_disj_lemma12, modularized proof of admI
1996-09-12 oheimb 1996-09-12 renamed adm_disj_lemma11 to adm_lemma11
1996-09-12 oheimb 1996-09-12 added comment on is_flat
1996-09-12 oheimb 1996-09-12 added stric tI
1996-09-12 oheimb 1996-09-12 undo last revision
1996-09-12 oheimb 1996-09-12 bin/isa2latex: copy the binary to bin/isa2latex instead of linking it there
1996-09-12 oheimb 1996-09-12 new \subsubsection{Configuring conversion tables and keyboard bindings} (by Franz Regensburger) added to the manual.
1996-09-12 paulson 1996-09-12 Tidied many proofs, using AddIffs to let equivalences take the place of separate Intr and Elim rules. Also deleted most named clasets.
1996-09-12 paulson 1996-09-12 Installed AddIffs, and some code from HOL.ML
1996-09-12 paulson 1996-09-12 Simplification and tidying of definitions
1996-09-12 paulson 1996-09-12 Now hologic.ML is loaded in HOL.ML
1996-09-12 paulson 1996-09-12 New file cladata.ML
1996-09-12 paulson 1996-09-12 Split off classical reasoning code to cladata.ML
1996-09-12 paulson 1996-09-12 Change to best_tac required to prevent looping
1996-09-11 paulson 1996-09-11 Moved RSLIST here from ../Relation.ML
1996-09-11 paulson 1996-09-11 Removal of univ_cs
1996-09-11 paulson 1996-09-11 Reformatting
1996-09-11 nipkow 1996-09-11 renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take uncertified things, because they need to be recertified anyway.
1996-09-11 nipkow 1996-09-11 Removed refs to clasets like rel_cs etc. Used implicit claset.
1996-09-10 nipkow 1996-09-10 Converted proofs to use default clasets.
1996-09-10 paulson 1996-09-10 Added Auth to the test target
1996-09-10 paulson 1996-09-10 Now runs all Auth proofs
1996-09-10 paulson 1996-09-10 Now uses DB-ROOT.ML, which is separate from ROOT.ML
1996-09-10 paulson 1996-09-10 Dedicated root file for making the Auth database
1996-09-10 paulson 1996-09-10 Beefed-up auto-tactic: now repeatedly simplifies if needed
1996-09-09 paulson 1996-09-09 "bad" set simplifies statements of many theorems
1996-09-09 nipkow 1996-09-09 added cterm_lift_inst_rule