src/HOL/Map.thy
changeset 53374 a14d2a854c02
parent 53015 a1119cf551e8
child 53820 9c7e97d67b45
     1.1 --- a/src/HOL/Map.thy	Tue Sep 03 00:51:08 2013 +0200
     1.2 +++ b/src/HOL/Map.thy	Tue Sep 03 01:12:40 2013 +0200
     1.3 @@ -715,18 +715,19 @@
     1.4      by (rule set_map_of_compr)
     1.5    ultimately show ?rhs by simp
     1.6  next
     1.7 -  assume ?rhs show ?lhs proof
     1.8 +  assume ?rhs show ?lhs
     1.9 +  proof
    1.10      fix k
    1.11      show "map_of xs k = map_of ys k" proof (cases "map_of xs k")
    1.12        case None
    1.13 -      moreover with `?rhs` have "map_of ys k = None"
    1.14 +      with `?rhs` have "map_of ys k = None"
    1.15          by (simp add: map_of_eq_None_iff)
    1.16 -      ultimately show ?thesis by simp
    1.17 +      with None show ?thesis by simp
    1.18      next
    1.19        case (Some v)
    1.20 -      moreover with distinct `?rhs` have "map_of ys k = Some v"
    1.21 +      with distinct `?rhs` have "map_of ys k = Some v"
    1.22          by simp
    1.23 -      ultimately show ?thesis by simp
    1.24 +      with Some show ?thesis by simp
    1.25      qed
    1.26    qed
    1.27  qed