src/HOL/Auth/Yahalom.ML
changeset 2156 9c361df93bd5
parent 2133 f00a688760b9
child 2160 ad4382e546fc
     1.1 --- a/src/HOL/Auth/Yahalom.ML	Fri Nov 01 18:28:19 1996 +0100
     1.2 +++ b/src/HOL/Auth/Yahalom.ML	Fri Nov 01 18:34:34 1996 +0100
     1.3 @@ -261,7 +261,7 @@
     1.4  by (etac yahalom.induct 1);
     1.5  by analz_Fake_tac;
     1.6  by (REPEAT_FIRST (resolve_tac [allI, analz_image_newK_lemma]));
     1.7 -by (ALLGOALS  (*Takes 26 secs*)
     1.8 +by (ALLGOALS
     1.9      (asm_simp_tac 
    1.10       (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
    1.11                           @ pushes)
    1.12 @@ -455,7 +455,7 @@
    1.13   "!!evs. evs : yahalom lost ==> EX NA' A' B'. ALL NA A B. \
    1.14  \      Crypt {|Agent A, Nonce NA, NB|} (shrK B) : parts(sees lost Spy evs) \
    1.15  \      --> B ~: lost --> NA = NA' & A = A' & B = B'";
    1.16 -by (parts_induct_tac 1);  (*TWO MINUTES*)
    1.17 +by (parts_induct_tac 1);  (*100 seconds??*)
    1.18  by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
    1.19  (*YM2: creation of new Nonce.  Move assertion into global context*)
    1.20  by (expand_case_tac "NB = ?y" 1);
    1.21 @@ -650,7 +650,7 @@
    1.22  \            : set_of_list evs)  |  Nonce NB : analz (sees lost Spy evs)";
    1.23  by (etac yahalom.induct 1);
    1.24  by analz_Fake_tac;
    1.25 -by (ALLGOALS  (*45 SECONDS*)
    1.26 +by (ALLGOALS  (*28 seconds*)
    1.27      (asm_simp_tac 
    1.28       (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
    1.29                            analz_image_newK,
    1.30 @@ -661,7 +661,7 @@
    1.31  by (fast_tac (!claset addss (!simpset)) 1);
    1.32  (*Fake*) (** LEVEL 4 **)
    1.33  by (spy_analz_tac 1);
    1.34 -(*YM1-YM3*)
    1.35 +(*YM1-YM3*) (*29 seconds*)
    1.36  by (EVERY (map grind_tac [3,2,1]));
    1.37  (*Oops*)
    1.38  by (Full_simp_tac 2);