| changeset 5143 | b94cd208f073 |
| parent 5069 | 3ea049f7979d |
| child 5183 | 89f162de39cf |
--- a/src/HOL/Map.ML Tue Jul 14 13:33:12 1998 +0200 +++ b/src/HOL/Map.ML Wed Jul 15 10:15:13 1998 +0200 @@ -108,7 +108,7 @@ qed "ran_empty"; Addsimps [ran_empty]; -Goalw [ran_def] "!!X. m a = None ==> ran(m[a|->b]) = insert b (ran m)"; +Goalw [ran_def] "m a = None ==> ran(m[a|->b]) = insert b (ran m)"; by Auto_tac; by (subgoal_tac "~(aa = a)" 1); by Auto_tac;