equal
deleted
inserted
replaced
854 [ (*push in occurrences of X...*) |
854 [ (*push in occurrences of X...*) |
855 (REPEAT o CHANGED) |
855 (REPEAT o CHANGED) |
856 (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1), |
856 (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1), |
857 (*...allowing further simplifications*) |
857 (*...allowing further simplifications*) |
858 simp_tac (!simpset setloop split_tac [expand_if]) 1, |
858 simp_tac (!simpset setloop split_tac [expand_if]) 1, |
859 REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI])), |
859 REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])), |
860 DEPTH_SOLVE |
860 DEPTH_SOLVE |
861 (REPEAT (Fake_insert_tac 1) THEN Asm_full_simp_tac 1 |
861 (REPEAT (Fake_insert_tac 1) THEN Asm_full_simp_tac 1 |
862 THEN |
862 THEN |
863 IF_UNSOLVED (Blast.depth_tac |
863 IF_UNSOLVED (Blast.depth_tac |
864 (!claset addIs [impOfSubs analz_mono, |
864 (!claset addIs [impOfSubs analz_mono, |