summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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