equal
deleted
inserted
replaced
854 DETERM |
854 DETERM |
855 (SELECT_GOAL |
855 (SELECT_GOAL |
856 (EVERY |
856 (EVERY |
857 [ (*push in occurrences of X...*) |
857 [ (*push in occurrences of X...*) |
858 (REPEAT o CHANGED) |
858 (REPEAT o CHANGED) |
859 (Rule_Insts.res_inst_tac ctxt [((("x", 1), Position.none), "X")] (insert_commute RS ssubst) 1), |
859 (Rule_Insts.res_inst_tac ctxt [((("x", 1), Position.none), "X")] [] |
|
860 (insert_commute RS ssubst) 1), |
860 (*...allowing further simplifications*) |
861 (*...allowing further simplifications*) |
861 simp_tac ctxt 1, |
862 simp_tac ctxt 1, |
862 REPEAT (FIRSTGOAL (resolve_tac ctxt [allI,impI,notI,conjI,iffI])), |
863 REPEAT (FIRSTGOAL (resolve_tac ctxt [allI,impI,notI,conjI,iffI])), |
863 DEPTH_SOLVE (atomic_spy_analz_tac ctxt 1)]) i); |
864 DEPTH_SOLVE (atomic_spy_analz_tac ctxt 1)]) i); |
864 *} |
865 *} |