expanded TABs
authorberghofe
Thu May 23 15:17:23 1996 +0200 (1996-05-23)
changeset 1763fb07e359b59f
parent 1762 6e481897a811
child 1764 69b93ffc29ec
expanded TABs
src/HOL/equalities.ML
     1.1 --- a/src/HOL/equalities.ML	Thu May 23 15:16:12 1996 +0200
     1.2 +++ b/src/HOL/equalities.ML	Thu May 23 15:17:23 1996 +0200
     1.3 @@ -87,7 +87,7 @@
     1.4   (fn _ => [Fast_tac 1]);
     1.5  
     1.6  goalw Set.thy [image_def]
     1.7 -"(%x. if P x then f x else g x) `` S			\
     1.8 +"(%x. if P x then f x else g x) `` S                    \
     1.9  \ = (f `` ({x.x:S & P x})) Un (g `` ({x.x:S & ~(P x)}))";
    1.10  by(split_tac [expand_if] 1);
    1.11  by(Fast_tac 1);
    1.12 @@ -102,8 +102,8 @@
    1.13  
    1.14  qed_goalw "image_range" Set.thy [image_def, range_def]
    1.15   "f``range g = range (%x. f (g x))" (fn _ => [
    1.16 -	rtac Collect_cong 1,
    1.17 -	Fast_tac 1]);
    1.18 +        rtac Collect_cong 1,
    1.19 +        Fast_tac 1]);
    1.20  
    1.21  section "Int";
    1.22