# HG changeset patch
# User paulson
# Date 867771253 -7200
# Node ID 1be4fee7606bc441bba939168d2a62f9528ed43a
# Parent  368206f85f4b6c5cb273c612f513a5247d6e745e
spy_analz_tac: Restored iffI to the list of rules used to break down
the subgoal

diff -r 368206f85f4b -r 1be4fee7606b src/HOL/Auth/Message.ML
--- a/src/HOL/Auth/Message.ML	Tue Jul 01 17:32:12 1997 +0200
+++ b/src/HOL/Auth/Message.ML	Tue Jul 01 17:34:13 1997 +0200
@@ -856,7 +856,7 @@
            (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1),
        (*...allowing further simplifications*)
        simp_tac (!simpset setloop split_tac [expand_if]) 1,
-       REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI])),
+       REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
        DEPTH_SOLVE 
          (REPEAT (Fake_insert_tac 1) THEN Asm_full_simp_tac 1
           THEN