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.
RuleInsts.res_inst_tac with proper context;
authorwenzelm
Wed, 11 Jun 2008 15:40:44 +0200
changeset 27147 62ab1968c1f4
parent 27146 443c19953137
child 27148 5b78e50adc49
RuleInsts.res_inst_tac with proper context;
doc-src/TutorialI/Protocol/Message.thy file | annotate | diff | comparison | revisions
src/HOL/Auth/Message.thy file | annotate | diff | comparison | revisions
src/HOL/SET-Protocol/MessageSET.thy file | annotate | diff | comparison | revisions 
--- a/doc-src/TutorialI/Protocol/Message.thy	Wed Jun 11 15:40:20 2008 +0200
+++ b/doc-src/TutorialI/Protocol/Message.thy	Wed Jun 11 15:40:44 2008 +0200
@@ -862,7 +862,8 @@
      (EVERY 
       [  (*push in occurrences of X...*)
        (REPEAT o CHANGED)
-           (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1),
+           (RuleInsts.res_inst_tac (Simplifier.the_context ss)
+            [(("x", 1), "X")] (insert_commute RS ssubst) 1),
        (*...allowing further simplifications*)
        simp_tac ss 1,
        REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
--- a/src/HOL/Auth/Message.thy	Wed Jun 11 15:40:20 2008 +0200
+++ b/src/HOL/Auth/Message.thy	Wed Jun 11 15:40:44 2008 +0200
@@ -882,7 +882,8 @@
      (EVERY 
       [  (*push in occurrences of X...*)
        (REPEAT o CHANGED)
-           (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1),
+           (RuleInsts.res_inst_tac (Simplifier.the_context ss)
+              [(("x", 1), "X")] (insert_commute RS ssubst) 1),
        (*...allowing further simplifications*)
        simp_tac ss 1,
        REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
--- a/src/HOL/SET-Protocol/MessageSET.thy	Wed Jun 11 15:40:20 2008 +0200
+++ b/src/HOL/SET-Protocol/MessageSET.thy	Wed Jun 11 15:40:44 2008 +0200
@@ -877,7 +877,8 @@
      (EVERY
       [  (*push in occurrences of X...*)
        (REPEAT o CHANGED)
-           (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1),
+           (RuleInsts.res_inst_tac (Simplifier.the_context ss)
+             [(("x", 1), "X")] (insert_commute RS ssubst) 1),
        (*...allowing further simplifications*)
        simp_tac ss 1,
        REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
isabelle