| changeset 5359 | bd539b72d484 |
| parent 5352 | a32312d17ed6 |
| child 5421 | 01fc8d6a40f2 |
--- a/src/HOL/Auth/Kerberos_BAN.ML Fri Aug 21 15:56:12 1998 +0200 +++ b/src/HOL/Auth/Kerberos_BAN.ML Fri Aug 21 16:14:34 1998 +0200 @@ -16,9 +16,6 @@ Tidied by lcp. *) -proof_timing:=true; -HOL_quantifiers := false; - AddEs spies_partsEs; AddDs [impOfSubs analz_subset_parts]; AddDs [impOfSubs Fake_parts_insert];