| changeset 5359 | bd539b72d484 |
| parent 5223 | 4cb05273f764 |
| child 5421 | 01fc8d6a40f2 |
--- a/src/HOL/Auth/NS_Public.ML Fri Aug 21 15:56:12 1998 +0200 +++ b/src/HOL/Auth/NS_Public.ML Fri Aug 21 16:14:34 1998 +0200 @@ -7,9 +7,6 @@ Version incorporating Lowe's fix (inclusion of B's identify in round 2). *) -set proof_timing; -HOL_quantifiers := false; - AddEs spies_partsEs; AddDs [impOfSubs analz_subset_parts]; AddDs [impOfSubs Fake_parts_insert];