changeset 13811 | f39f67982854 |
parent 11015 | 55d95834c815 |
child 13890 | 90611b4e0054 |
--- a/src/HOL/Map.ML Fri Feb 07 16:40:23 2003 +0100 +++ b/src/HOL/Map.ML Sat Feb 08 14:46:22 2003 +0100 @@ -221,7 +221,12 @@ Goalw [dom_def] "a : dom m ==> ? b. m a = Some b"; by Auto_tac; qed "domD"; -AddSDs [domD]; + +Goalw [dom_def] "(a : dom m) = (m a ~= None)"; +by Auto_tac; +qed "domIff"; +AddIffs [domIff]; +Delsimps [domIff]; Goalw [dom_def] "dom empty = {}"; by (Simp_tac 1);