Greatly simplified the proof of A_can_trust

Working again with new theory Shared

Simplified main theorem by abstracting out newK

Moved sees_lost_agent_subset_sees_Spy to common file, and simplified main thm

Moved sees_lost_agent_subset_sees_Spy to common file

Added new guarantees for A and B

added shyps comment;

Inserted check for rewrite rules which introduce extra Vars on the rhs.

Removed some dead wood. Transferred lemmas used to prove analz_image_newK to Shared.ML

Improved discussion of shyps thanks to Markus Wenzel

prune_params_tac no longer rewrites main goal

Added catch-all clause to drop, preventing exception Match

Now replaces uses of ssubst by stac

Documented sort hypotheses and improved discussion of derivations

Documented defer_tac and moved back the obsolete tactics like fold_tac

Documented stac, and updated the documentation of hyp_subst_tac

Declared stac

Ran expandshort; used stac instead of ssubst

Ran expandshort; used stac instead of ssubst

Ran expandshort; used stac instead of ssubst

Ran expandshort; used stac instead of ssubst

Introduction of "lost" argument Changed Enemy -> Spy Ran expandshort

Ran expandshort

Changed freeze to freeze_thaw

Generalized freeze to freeze_thaw in order to implement defer_tac

Last working version prior to addition of "lost" component

Last working version before "lost"

Last working version prior to introduction of "lost"

Prevention of Overflow exception (for SML/NJ) in gensym

Rationalized the rewriting of membership for {} and insert by deleting the redundant theorems in_empty and in_insert