src/HOL/Set_Interval.thy
changeset 55085 0e8e4dc55866
parent 54606 0cb8a2defb06
child 55088 57c82e01022b
     1.1 --- a/src/HOL/Set_Interval.thy	Mon Jan 20 20:42:43 2014 +0100
     1.2 +++ b/src/HOL/Set_Interval.thy	Mon Jan 20 21:32:41 2014 +0100
     1.3 @@ -827,8 +827,8 @@
     1.4  subset is exactly that interval. *}
     1.5  
     1.6  lemma subset_card_intvl_is_intvl:
     1.7 -  assumes "A \<subseteq> {k..<k+card A}"
     1.8 -  shows "A = {k..<k+card A}"
     1.9 +  assumes "A \<subseteq> {k..<k + card A}"
    1.10 +  shows "A = {k..<k + card A}"
    1.11  proof (cases "finite A")
    1.12    case True
    1.13    from this and assms show ?thesis
    1.14 @@ -837,7 +837,7 @@
    1.15    next
    1.16      case (insert b A)
    1.17      hence *: "b \<notin> A" by auto
    1.18 -    with insert have "A <= {k..<k+card A}" and "b = k+card A"
    1.19 +    with insert have "A <= {k..<k + card A}" and "b = k + card A"
    1.20        by fastforce+
    1.21      with insert * show ?case by auto
    1.22    qed