equal
deleted
inserted
replaced
864 DETERM |
864 DETERM |
865 (SELECT_GOAL |
865 (SELECT_GOAL |
866 (EVERY |
866 (EVERY |
867 [ (*push in occurrences of X...*) |
867 [ (*push in occurrences of X...*) |
868 (REPEAT o CHANGED) |
868 (REPEAT o CHANGED) |
869 (res_inst_tac ctxt [((("x", 1), Position.none), "X")] (insert_commute RS ssubst) 1), |
869 (Rule_Insts.res_inst_tac ctxt [((("x", 1), Position.none), "X")] (insert_commute RS ssubst) 1), |
870 (*...allowing further simplifications*) |
870 (*...allowing further simplifications*) |
871 simp_tac ctxt 1, |
871 simp_tac ctxt 1, |
872 REPEAT (FIRSTGOAL (resolve_tac ctxt [allI,impI,notI,conjI,iffI])), |
872 REPEAT (FIRSTGOAL (resolve_tac ctxt [allI,impI,notI,conjI,iffI])), |
873 DEPTH_SOLVE (atomic_spy_analz_tac ctxt 1)]) i); |
873 DEPTH_SOLVE (atomic_spy_analz_tac ctxt 1)]) i); |
874 *} |
874 *} |