| changeset 4838 | 196100237656 |
| parent 4686 | 74a12e86b20b |
| child 4883 | c1aec06d1dca |
--- a/src/HOL/Map.ML Mon Apr 27 19:30:40 1998 +0200 +++ b/src/HOL/Map.ML Mon Apr 27 19:32:19 1998 +0200 @@ -63,9 +63,8 @@ goal thy "map_of xs k = Some y --> (k,y):set xs"; by (list.induct_tac "xs" 1); by (Simp_tac 1); +by (split_all_tac 1); by (Asm_simp_tac 1); -by (split_all_tac 1); -by (Simp_tac 1); qed_spec_mp "map_of_SomeD"; section "dom";