src/HOL/Auth/Recur.ML
changeset 7057 b9ddbb925939
parent 5535 678999604ee9
child 7499 23e090051cb8
equal deleted inserted replaced
7056:522a7013d7df 7057:b9ddbb925939
   366 (** LEVEL 5 **)
   366 (** LEVEL 5 **)
   367 by (Blast_tac 1);
   367 by (Blast_tac 1);
   368 by (REPEAT_FIRST (resolve_tac [allI, conjI, impI]));
   368 by (REPEAT_FIRST (resolve_tac [allI, conjI, impI]));
   369 by (ALLGOALS Clarify_tac);
   369 by (ALLGOALS Clarify_tac);
   370 by (blast_tac (claset() addSDs  [resp_analz_insert]
   370 by (blast_tac (claset() addSDs  [resp_analz_insert]
   371  		        addIs  [impOfSubs analz_subset_parts]) 2);
   371  		        addIs  [impOfSubs analz_subset_parts]) 3);
   372 by (blast_tac (claset() addSDs [respond_certificate]) 1);
   372 by (blast_tac (claset() addSDs [respond_certificate]) 2);
   373 by (Asm_full_simp_tac 1);
   373 by (Asm_full_simp_tac 1);
   374 (*by unicity, either B=Aa or B=A', a contradiction if B: bad*)
   374 (*by unicity, either B=Aa or B=A', a contradiction if B: bad*)
   375 by (blast_tac
   375 by (blast_tac
   376     (claset() addSEs [MPair_parts]
   376     (claset() addSEs [MPair_parts]
   377 	     addDs [parts.Body,
   377 	     addDs [parts.Body,
   393 (*RA2*)
   393 (*RA2*)
   394 by (spy_analz_tac 3);
   394 by (spy_analz_tac 3);
   395 (*Fake*)
   395 (*Fake*)
   396 by (spy_analz_tac 2);
   396 by (spy_analz_tac 2);
   397 (*Base*)
   397 (*Base*)
   398 by (Blast_tac 1);
   398 by (Force_tac 1);
   399 (*RA3 remains*)
   399 (*RA3 remains*)
   400 by (simp_tac (simpset() addsimps [parts_insert_spies]) 1);
   400 by (simp_tac (simpset() addsimps [parts_insert_spies]) 1);
   401 by (safe_tac (claset() delrules [impCE]));
   401 by (safe_tac (claset() delrules [impCE]));
   402 (*RA3, case 2: K is an old key*)
   402 (*RA3, case 2: K is an old key*)
   403 by (blast_tac (claset() addSDs [resp_analz_insert]
   403 by (blast_tac (claset() addSDs [resp_analz_insert]