# HG changeset patch
# User berghofe
# Date 832857443 -7200
# Node ID fb07e359b59f90d68f7c5fa9d1655126fa2704de
# Parent  6e481897a811188985bcd3a939097513dd25987c
expanded TABs

diff -r 6e481897a811 -r fb07e359b59f src/HOL/equalities.ML
--- 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";