1996-09-11 paulson Reformatting
1996-09-11 nipkow renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take
1996-09-11 nipkow Removed refs to clasets like rel_cs etc. Used implicit claset.
1996-09-10 nipkow Converted proofs to use default clasets.
1996-09-10 paulson Added Auth to the test target
1996-09-10 paulson Now runs all Auth proofs
1996-09-10 paulson Now uses DB-ROOT.ML, which is separate from ROOT.ML
1996-09-10 paulson Dedicated root file for making the Auth database
1996-09-10 paulson Beefed-up auto-tactic: now repeatedly simplifies if needed
1996-09-09 paulson "bad" set simplifies statements of many theorems
1996-09-09 nipkow added cterm_lift_inst_rule
1996-09-09 paulson Stronger proofs; work for Otway-Rees
1996-09-09 paulson Stronger proofs; work for Otway-Rees
1996-09-09 paulson These simpsets must not use miniscoping
1996-09-09 paulson Corrected associativity: must be to right, as the type dictatess
1996-09-09 paulson Removal of (EX x. P) <-> P and (ALL x. P) <-> P
1996-09-06 paulson Improved error handling: if there are syntax or type-checking
1996-09-06 paulson Modified proof to work with miniscoping
1996-09-05 paulson Now uses thin_tac
1996-09-05 paulson Now uses thin_tac
1996-09-05 paulson Renaming of _rews to _simps
1996-09-05 paulson Added thin_tac to signature; previous change was useless
1996-09-05 paulson Some renaming. Note that this miniscoping is more
1996-09-05 paulson Introduction of miniscoping for FOL
1996-09-05 paulson Pretty-printing change to emphasize the scope of assumptions
1996-09-05 paulson Declared thin_tac
1996-09-05 paulson Miniscoping rules are deleted, as these brittle proofs
1996-09-05 paulson Simplified some proofs for compatibility with miniscoping
1996-09-05 paulson Added miniscoping to the simplifier: quantifiers are now pushed in
1996-09-03 paulson Fixed pretty-printing of {|...|}
1996-09-03 paulson New theorems for Fake case
1996-09-03 paulson A further tidying
1996-09-03 paulson ROOT file for Auth directory
1996-09-03 paulson Renaming and simplification
1996-09-03 paulson Renaming and simplification
1996-09-03 paulson Initial working proof of Otway-Rees protocol
1996-08-23 nipkow Swaped two conditions in the completeness statement.
1996-08-23 nipkow Generalized my_lemma1: (c3,s3) |--> cs3
1996-08-22 paulson Now deepen_tac can take advantage of wrappers --
1996-08-22 paulson Proved mem_if
1996-08-22 paulson Proved set_of_list_subset_Cons
1996-08-22 paulson For building the security theory as a separate database
1996-08-21 paulson Separation of theory Event into two parts:
1996-08-21 paulson Addition of message NS5
1996-08-21 paulson Tidying: removing redundant args in classical reasoner calls
1996-08-21 paulson Added le_eq_less_Suc; fixed some comments;
1996-08-20 paulson Working version of NS, messages 1-4!
1996-08-20 paulson Working version of NS, messages 1-3, WITH INTERLEAVING
1996-08-20 paulson Added ref to allow suppression of error msgs
1996-08-20 paulson New classical reasoner: warns of, and ignores, redundant rules.
1996-08-20 paulson Addition of function set_of_list
1996-08-20 paulson Some tidying. This brittle proof depends upon
1996-08-20 paulson Corrected for new classical reasoner: redundant rules
1996-08-19 nipkow updated html-link
1996-08-19 paulson Installation of auto_tac; re-organization
1996-08-19 paulson Tidied up the proofs
1996-08-19 paulson Added impOfSubs
1996-08-19 paulson Now less_zeroE is a Safe Elim rule
1996-08-19 paulson Improved comment
1996-08-19 paulson Added proof of Un_insert_right
(0) -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip