Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
spy_analz_tac: Restored iffI to the list of rules used to break down
authorpaulson
Tue, 01 Jul 1997 17:34:13 +0200
changeset 3476 1be4fee7606b
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 file | annotate | diff | comparison | revisions 
--- 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
isabelle