19971224 
paulson 
19971224 
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort

file  diff  annotate 
19971223 
paulson 
19971223 
Tidied using more default rules

file  diff  annotate 
19971219 
wenzelm 
19971219 
tuned;

file  diff  annotate 
19971216 
paulson 
19971216 
Simplified proofs using rewrites for f``A where f is injective

file  diff  annotate 
19971111 
paulson 
19971111 
Made some proofs more robust

file  diff  annotate 
19971103 
wenzelm 
19971103 
isatool fixclasimp;

file  diff  annotate 
19971017 
nipkow 
19971017 
setloop split_tac > addsplits

file  diff  annotate 
19970925 
paulson 
19970925 
Tidied proofs, using Clarify_tac

file  diff  annotate 
19970918 
paulson 
19970918 
Global change: lost>bad and sees Spy>spies
First change just gives a more sensible name.
Second change eliminates the agent parameter of "sees" to simplify
definitions and theorems

file  diff  annotate 
19970916 
paulson 
19970916 
Deleted the redundant simprule not_parts_not_analz

file  diff  annotate 
19970714 
paulson 
19970714 
Changing "lost" from a parameter of protocol definitions to a constant.
Advantages: no "lost" argument everywhere; fewer Vars in subgoals;
less need for specially instantiated rules
Disadvantage: can no longer prove "Agent_not_see_encrypted_key", but this
theorem was never used, and its original proof was also broken
the introduction of the "Notes" constructor.

file  diff  annotate 
19970711 
paulson 
19970711 
Removal of monotonicity reasoning involving "lost" and the theorem
Agent_not_see_encrypted_key, which (a) is never used and (b) becomes harder
to prove when Notes is available.

file  diff  annotate 
19970627 
paulson 
19970627 
Corrected indentations and margins after the renaming of "set_of_list"

file  diff  annotate 
19970626 
nipkow 
19970626 
set_of_list > set

file  diff  annotate 
19970507 
paulson 
19970507 
Conversion to use blast_tac (with other improvements)

file  diff  annotate 
19970215 
oheimb 
19970215 
reflecting my recent changes of the simplifier and classical reasoner

file  diff  annotate 
19970123 
paulson 
19970123 
Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()

file  diff  annotate 
19970117 
paulson 
19970117 
Now with Andy Gordon's treatment of freshness to replace newN/K

file  diff  annotate 
19970109 
paulson 
19970109 
New treatment of nonce creation

file  diff  annotate 
19970107 
paulson 
19970107 
Tidied up the unicity proofs

file  diff  annotate 
19961219 
paulson 
19961219 
Extensive tidying and simplification, largely stemming from
changing newN and newK to take an integer argument

file  diff  annotate 
19961216 
paulson 
19961216 
New tactics: prove_unique_tac and analz_induct_tac

file  diff  annotate 
19961213 
paulson 
19961213 
Streamlined many proofs

file  diff  annotate 
19961205 
paulson 
19961205 
Minor speedups

file  diff  annotate 
19961205 
paulson 
19961205 
Publickey examples

file  diff  annotate 