src/HOL/SET-Protocol/Merchant_Registration.thy
changeset 24123 a0fc58900606
parent 23755 1c4672d130b1
child 32960 69916a850301
--- a/src/HOL/SET-Protocol/Merchant_Registration.thy	Wed Aug 01 20:25:16 2007 +0200
+++ b/src/HOL/SET-Protocol/Merchant_Registration.thy	Wed Aug 01 21:10:36 2007 +0200
@@ -289,7 +289,7 @@
          add: analz_image_keys_simps abbrev_simps analz_knows_absorb
               analz_knows_absorb2 analz_Key_image_insert_eq notin_image_iff
               Spy_analz_private_Key analz_image_priEK)
-  --{*23 seconds on a 1.8GHz machine*}
+  --{*5 seconds on a 1.6GHz machine*}
 apply spy_analz  --{*Fake*}
 apply auto  --{*Message 3*}
 done