Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Doc/Tutorial/Protocol/Message.thy
changeset 59763 56d2c357e6b5
parent 59755 f8d164ab0dc1
child 59780 23b67731f4f0 
--- a/src/Doc/Tutorial/Protocol/Message.thy	Fri Mar 20 11:53:22 2015 +0100
+++ b/src/Doc/Tutorial/Protocol/Message.thy	Fri Mar 20 14:48:04 2015 +0100
@@ -856,7 +856,7 @@
      (EVERY 
       [  (*push in occurrences of X...*)
        (REPEAT o CHANGED)
-           (res_inst_tac ctxt [((("x", 1), Position.none), "X")] (insert_commute RS ssubst) 1),
+         (Rule_Insts.res_inst_tac ctxt [((("x", 1), Position.none), "X")] (insert_commute RS ssubst) 1),
        (*...allowing further simplifications*)
        simp_tac ctxt 1,
        REPEAT (FIRSTGOAL (resolve_tac ctxt [allI,impI,notI,conjI,iffI])),
isabelle