src/HOL/Auth/Message.ML
changeset 2559 06b6a499f8ae
parent 2516 4d68fbe6378b
child 2637 e9b203f854ae
equal deleted inserted replaced
2558:6e8d130463e3 2559:06b6a499f8ae
   866 fun prove_unique_tac lemma = 
   866 fun prove_unique_tac lemma = 
   867   EVERY' [dtac lemma,
   867   EVERY' [dtac lemma,
   868           REPEAT o (mp_tac ORELSE' eresolve_tac [asm_rl,exE]),
   868           REPEAT o (mp_tac ORELSE' eresolve_tac [asm_rl,exE]),
   869           (*Duplicate the assumption*)
   869           (*Duplicate the assumption*)
   870           forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl,
   870           forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl,
   871           fast_tac (!claset addSDs [spec])];
   871           depth_tac (!claset addSDs [spec]) 0];
   872 
   872 
   873 
   873 
   874 (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
   874 (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
   875 goal Set.thy "A Un (B Un A) = B Un A";
   875 goal Set.thy "A Un (B Un A) = B Un A";
   876 by (Fast_tac 1);
   876 by (Fast_tac 1);