# HG changeset patch
# User paulson
# Date 1087289193 -7200
# Node ID 7bfe4fa8a88f50aac051ee2425f0efbc6f927eee
# Parent  efbaecbdc05c5d1ded629fc39a59198c5c289caa
slight speed improvement

diff -r efbaecbdc05c -r 7bfe4fa8a88f src/HOL/Auth/KerberosIV.thy
--- a/src/HOL/Auth/KerberosIV.thy	Tue Jun 15 10:40:05 2004 +0200
+++ b/src/HOL/Auth/KerberosIV.thy	Tue Jun 15 10:46:33 2004 +0200
@@ -855,12 +855,14 @@
 apply (case_tac [11] "KeyCryptKey AuthKey SK evsO1")
 apply (case_tac [8] "KeyCryptKey ServKey SK evs5")
 apply (simp_all del: image_insert
-          add: analz_image_freshK_simps KeyCryptKey_Says shrK_not_KeyCryptKey
+          add: analz_image_freshK_simps KeyCryptKey_Says)
+txt{*Fake*} 
+apply spy_analz
+apply (simp_all del: image_insert
+          add: shrK_not_KeyCryptKey
                Oops2_not_KeyCryptKey Auth_fresh_not_KeyCryptKey
                Serv_fresh_not_KeyCryptKey Says_Tgs_KeyCryptKey Spy_analz_shrK)
-  --{*18 seconds on a 1.8GHz machine??*}
-txt{*Fake*} 
-apply spy_analz
+  --{*Splitting the @{text simp_all} into two parts makes it faster.*}
 txt{*K2*}
 apply blast 
 txt{*K3*}