src/HOL/Auth/NS_Public_Bad.ML

 From page 260 of
   Burrows, Abadi and Needham.  A Logic of Authentication.
   Proc. Royal Soc. 426 (1989)
 *)
 
-open NS_Public_Bad;
-
-set proof_timing;
 HOL_quantifiers := false;
 
 AddEs spies_partsEs;
 AddDs [impOfSubs analz_subset_parts];
 AddDs [impOfSubs Fake_parts_insert];