equal
deleted
inserted
replaced
878 DETERM |
878 DETERM |
879 (SELECT_GOAL |
879 (SELECT_GOAL |
880 (EVERY |
880 (EVERY |
881 [ (*push in occurrences of X...*) |
881 [ (*push in occurrences of X...*) |
882 (REPEAT o CHANGED) |
882 (REPEAT o CHANGED) |
883 (RuleInsts.res_inst_tac (Simplifier.the_context ss) |
883 (res_inst_tac (Simplifier.the_context ss) |
884 [(("x", 1), "X")] (insert_commute RS ssubst) 1), |
884 [(("x", 1), "X")] (insert_commute RS ssubst) 1), |
885 (*...allowing further simplifications*) |
885 (*...allowing further simplifications*) |
886 simp_tac ss 1, |
886 simp_tac ss 1, |
887 REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])), |
887 REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])), |
888 DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i) |
888 DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i) |