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
1996-09-09 paulson 1996-09-09 Stronger proofs; work for Otway-Rees
1996-09-09 paulson 1996-09-09 Stronger proofs; work for Otway-Rees
1996-09-09 paulson 1996-09-09 These simpsets must not use miniscoping
1996-09-09 paulson 1996-09-09 Corrected associativity: must be to right, as the type dictatess
1996-09-09 paulson 1996-09-09 Removal of (EX x. P) <-> P and (ALL x. P) <-> P from ex_simps and all_simps. as they are already in quant_simps.
1996-09-06 paulson 1996-09-06 Improved error handling: if there are syntax or type-checking errors, prints the name of the offending axiom
1996-09-06 paulson 1996-09-06 Modified proof to work with miniscoping
1996-09-05 paulson 1996-09-05 Now uses thin_tac
1996-09-05 paulson 1996-09-05 Now uses thin_tac
1996-09-05 paulson 1996-09-05 Renaming of _rews to _simps
1996-09-05 paulson 1996-09-05 Added thin_tac to signature; previous change was useless
1996-09-05 paulson 1996-09-05 Some renaming. Note that this miniscoping is more general than that of ../simpdata.ML, as distributive laws are included. On this other hand this version is for NNF only.
1996-09-05 paulson 1996-09-05 Introduction of miniscoping for FOL
1996-09-05 paulson 1996-09-05 Pretty-printing change to emphasize the scope of assumptions
1996-09-05 paulson 1996-09-05 Declared thin_tac
1996-09-05 paulson 1996-09-05 Miniscoping rules are deleted, as these brittle proofs would otherwise have to be entirely redone
1996-09-05 paulson 1996-09-05 Simplified some proofs for compatibility with miniscoping
1996-09-05 paulson 1996-09-05 Added miniscoping to the simplifier: quantifiers are now pushed in
1996-09-03 paulson 1996-09-03 Fixed pretty-printing of {|...|}
1996-09-03 paulson 1996-09-03 New theorems for Fake case
1996-09-03 paulson 1996-09-03 A further tidying
1996-09-03 paulson 1996-09-03 ROOT file for Auth directory
1996-09-03 paulson 1996-09-03 Renaming and simplification
1996-09-03 paulson 1996-09-03 Renaming and simplification
1996-09-03 paulson 1996-09-03 Initial working proof of Otway-Rees protocol
1996-08-23 nipkow 1996-08-23 Swaped two conditions in the completeness statement.
1996-08-23 nipkow 1996-08-23 Generalized my_lemma1: (c3,s3) |--> cs3
1996-08-22 paulson 1996-08-22 Now deepen_tac can take advantage of wrappers -- including addss...