equal
deleted
inserted
replaced
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) |