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.
Replacing impOfSubs analz_mono by analz_insertI should improve convergence
authorpaulson
Thu, 21 Aug 1997 12:56:29 +0200
changeset 3650 282ffdc91884
parent 3649 e530286d4847
child 3651 5f6ab7fbd53b
Replacing impOfSubs analz_mono by analz_insertI should improve convergence of spy_analz_tac
src/HOL/Auth/Message.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Auth/Message.ML	Thu Aug 21 12:55:10 1997 +0200
+++ b/src/HOL/Auth/Message.ML	Thu Aug 21 12:56:29 1997 +0200
@@ -884,7 +884,7 @@
          (REPEAT (Fake_insert_tac 1) THEN Asm_full_simp_tac 1
           THEN
           IF_UNSOLVED (Blast.depth_tac
-		       (!claset addIs [impOfSubs analz_mono,
+		       (!claset addIs [analz_insertI,
 				       impOfSubs analz_subset_parts]) 2 1))
        ]) i);
isabelle