changeset 62390 | 842917225d56 |
parent 62379 | 340738057c8c |
child 62789 | ce15dd971965 |
--- a/src/HOL/Set_Interval.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Set_Interval.thy Tue Feb 23 16:25:08 2016 +0100 @@ -929,7 +929,7 @@ by (auto intro!: image_eqI[of _ _ "a + c"]) next assume "\<not> c < y" with a show ?thesis - by (auto intro!: image_eqI[of _ _ x] split: split_if_asm) + by (auto intro!: image_eqI[of _ _ x] split: if_split_asm) qed qed auto