spy_analz_tac: Restored iffI to the list of rules used to break down
authorpaulson
Tue Jul 01 17:34:13 1997 +0200 (1997-07-01)
changeset 34761be4fee7606b
parent 3475 368206f85f4b
child 3477 3aced7fa7d8b
spy_analz_tac: Restored iffI to the list of rules used to break down
the subgoal
src/HOL/Auth/Message.ML
     1.1 --- a/src/HOL/Auth/Message.ML	Tue Jul 01 17:32:12 1997 +0200
     1.2 +++ b/src/HOL/Auth/Message.ML	Tue Jul 01 17:34:13 1997 +0200
     1.3 @@ -856,7 +856,7 @@
     1.4             (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1),
     1.5         (*...allowing further simplifications*)
     1.6         simp_tac (!simpset setloop split_tac [expand_if]) 1,
     1.7 -       REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI])),
     1.8 +       REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
     1.9         DEPTH_SOLVE 
    1.10           (REPEAT (Fake_insert_tac 1) THEN Asm_full_simp_tac 1
    1.11            THEN