doc-src/TutorialI/Protocol/Message.thy
changeset 27239 f2f42f9fa09d
parent 27225 b316dde851f5
child 30509 e19d5b459a61
equal deleted inserted replaced
27238:d2bf12727c8a 27239:f2f42f9fa09d
   862   DETERM
   862   DETERM
   863    (SELECT_GOAL
   863    (SELECT_GOAL
   864      (EVERY 
   864      (EVERY 
   865       [  (*push in occurrences of X...*)
   865       [  (*push in occurrences of X...*)
   866        (REPEAT o CHANGED)
   866        (REPEAT o CHANGED)
   867            (RuleInsts.res_inst_tac (Simplifier.the_context ss)
   867            (res_inst_tac (Simplifier.the_context ss)
   868             [(("x", 1), "X")] (insert_commute RS ssubst) 1),
   868             [(("x", 1), "X")] (insert_commute RS ssubst) 1),
   869        (*...allowing further simplifications*)
   869        (*...allowing further simplifications*)
   870        simp_tac ss 1,
   870        simp_tac ss 1,
   871        REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
   871        REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
   872        DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i)
   872        DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i)