--- a/src/HOL/equalities.ML Thu May 23 15:16:12 1996 +0200
+++ b/src/HOL/equalities.ML Thu May 23 15:17:23 1996 +0200
@@ -87,7 +87,7 @@
(fn _ => [Fast_tac 1]);
goalw Set.thy [image_def]
-"(%x. if P x then f x else g x) `` S \
+"(%x. if P x then f x else g x) `` S \
\ = (f `` ({x.x:S & P x})) Un (g `` ({x.x:S & ~(P x)}))";
by(split_tac [expand_if] 1);
by(Fast_tac 1);
@@ -102,8 +102,8 @@
qed_goalw "image_range" Set.thy [image_def, range_def]
"f``range g = range (%x. f (g x))" (fn _ => [
- rtac Collect_cong 1,
- Fast_tac 1]);
+ rtac Collect_cong 1,
+ Fast_tac 1]);
section "Int";