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