diff -r ea830f6e3c2d -r 2f86b403d975 src/HOL/Auth/TLS.ML --- a/src/HOL/Auth/TLS.ML Thu Sep 25 12:19:41 1997 +0200 +++ b/src/HOL/Auth/TLS.ML Thu Sep 25 12:20:24 1997 +0200 @@ -253,7 +253,7 @@ \ |] ==> Crypt (pubK B) (Nonce PMS) : parts (spies evs)"; by (etac rev_mp 1); by (parts_induct_tac 1); -by clarify_tac; +by (ALLGOALS Clarify_tac); (*Fake*) by (blast_tac (!claset addIs [parts_insertI]) 1); (*Client, Server Accept*) @@ -610,7 +610,7 @@ \ Says A' B' (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs --> \ \ A = A'"; by (analz_induct_tac 1); (*17 seconds*) -by clarify_tac; +by (ALLGOALS Clarify_tac); (*ClientFinished, ClientResume: by unicity of PMS*) by (REPEAT (blast_tac (!claset addSDs [Notes_master_imp_Notes_PMS] @@ -632,7 +632,7 @@ by (etac tls.induct 1); (*This roundabout proof sequence avoids looping in simplification*) by (ALLGOALS Simp_tac); -by clarify_tac; +by (ALLGOALS Clarify_tac); by (Fake_parts_insert_tac 1); by (ALLGOALS Asm_simp_tac); (*Oops*) @@ -654,7 +654,7 @@ \ Says B' A' (Crypt (serverK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs --> \ \ B = B'"; by (analz_induct_tac 1); (*17 seconds*) -by clarify_tac; +by (ALLGOALS Clarify_tac); (*ServerResume, ServerFinished: by unicity of PMS*) by (REPEAT (blast_tac (!claset addSEs [MPair_parts] @@ -679,7 +679,7 @@ by (etac tls.induct 1); (*This roundabout proof sequence avoids looping in simplification*) by (ALLGOALS Simp_tac); -by clarify_tac; +by (ALLGOALS Clarify_tac); by (Fake_parts_insert_tac 1); by (ALLGOALS Asm_simp_tac); (*Oops*) @@ -711,9 +711,8 @@ by (hyp_subst_tac 1); by (analz_induct_tac 1); (*27 seconds*) by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib]))); -by clarify_tac; -(*ServerResume*) -by (Blast_tac 3); +(*proves ServerResume*) +by (ALLGOALS Clarify_tac); (*ClientCertKeyEx*) by (fast_tac (*blast_tac gives PROOF FAILED*) (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]) 2); @@ -758,7 +757,7 @@ by (hyp_subst_tac 1); by (analz_induct_tac 1); (*20 seconds*) by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib]))); -by clarify_tac; +by (ALLGOALS Clarify_tac); (*ServerResume, ServerFinished: by unicity of PMS*) by (REPEAT (blast_tac (!claset addSEs [MPair_parts] @@ -805,7 +804,7 @@ \ Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y : parts (spies evs) --> \ \ Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs"; by (analz_induct_tac 1); (*23 seconds*) -by clarify_tac; +by (ALLGOALS Clarify_tac); (*ClientFinished, ClientResume: by unicity of PMS*) by (REPEAT (blast_tac (!claset delrules [conjI] addSDs [Notes_master_imp_Notes_PMS] @@ -852,5 +851,6 @@ qed "AuthClientFinished"; (*22/9/97: loads in 622s, which is 10 minutes 22 seconds*) +(*24/9/97: loads in 672s, which is 11 minutes 12 seconds [stronger theorems]*)