src/HOL/equalities.ML
changeset 1660 8cb42cd97579
parent 1618 372880456b5b
child 1748 88650ba93c10
     1.1 --- a/src/HOL/equalities.ML	Wed Apr 17 11:46:10 1996 +0200
     1.2 +++ b/src/HOL/equalities.ML	Wed Apr 17 17:59:58 1996 +0200
     1.3 @@ -69,7 +69,7 @@
     1.4  by (fast_tac eq_cs 1);
     1.5  qed "mk_disjoint_insert";
     1.6  
     1.7 -section "''";
     1.8 +section "``";
     1.9  
    1.10  goal Set.thy "f``{} = {}";
    1.11  by (fast_tac eq_cs 1);
    1.12 @@ -81,6 +81,19 @@
    1.13  qed "image_insert";
    1.14  Addsimps[image_insert];
    1.15  
    1.16 +qed_goal "ball_image" Set.thy "(!y:F``S. P y) = (!x:S. P (F x))"
    1.17 + (fn _ => [fast_tac set_cs 1]);
    1.18 +
    1.19 +section "range";
    1.20 +
    1.21 +qed_goal "ball_range" Set.thy "(!y:range f. P y) = (!x. P (f x))"
    1.22 + (fn _ => [fast_tac set_cs 1]);
    1.23 +
    1.24 +qed_goalw "image_range" Set.thy [image_def, range_def]
    1.25 + "f``range g = range (%x. f (g x))" (fn _ => [
    1.26 +	rtac Collect_cong 1,
    1.27 +	fast_tac set_cs 1]);
    1.28 +
    1.29  section "Int";
    1.30  
    1.31  goal Set.thy "A Int A = A";