src/HOL/Sum.ML
changeset 1465 5d7a7e439cec
parent 1264 3eb91524b938
child 1515 4ed79ebab64d
     1.1 --- a/src/HOL/Sum.ML	Tue Jan 30 15:19:20 1996 +0100
     1.2 +++ b/src/HOL/Sum.ML	Tue Jan 30 15:24:36 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	HOL/Sum.ML
     1.5 +(*  Title:      HOL/Sum.ML
     1.6      ID:         $Id$
     1.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.9      Copyright   1991  University of Cambridge
    1.10  
    1.11  For Sum.thy.  The disjoint sum of two types
    1.12 @@ -28,9 +28,9 @@
    1.13  
    1.14  goalw Sum.thy [Inl_Rep_def, Inr_Rep_def] "Inl_Rep(a) ~= Inr_Rep(b)";
    1.15  by (EVERY1 [rtac notI,
    1.16 -	    etac (fun_cong RS fun_cong RS fun_cong RS iffE), 
    1.17 -	    rtac (notE RS ccontr),  etac (mp RS conjunct2), 
    1.18 -	    REPEAT o (ares_tac [refl,conjI]) ]);
    1.19 +            etac (fun_cong RS fun_cong RS fun_cong RS iffE), 
    1.20 +            rtac (notE RS ccontr),  etac (mp RS conjunct2), 
    1.21 +            REPEAT o (ares_tac [refl,conjI]) ]);
    1.22  qed "Inl_Rep_not_Inr_Rep";
    1.23  
    1.24  goalw Sum.thy [Inl_def,Inr_def] "Inl(a) ~= Inr(b)";
    1.25 @@ -136,14 +136,14 @@
    1.26  by (rtac (rewrite_rule [Sum_def] Rep_Sum RS CollectE) 1);
    1.27  by (REPEAT (eresolve_tac [disjE,exE] 1
    1.28       ORELSE EVERY1 [resolve_tac prems, 
    1.29 -		    etac subst,
    1.30 -		    rtac (Rep_Sum_inverse RS sym)]));
    1.31 +                    etac subst,
    1.32 +                    rtac (Rep_Sum_inverse RS sym)]));
    1.33  qed "sumE";
    1.34  
    1.35  goal Sum.thy "sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)";
    1.36  by (EVERY1 [res_inst_tac [("s","s")] sumE, 
    1.37 -	    etac ssubst, rtac sum_case_Inl,
    1.38 -	    etac ssubst, rtac sum_case_Inr]);
    1.39 +            etac ssubst, rtac sum_case_Inl,
    1.40 +            etac ssubst, rtac sum_case_Inr]);
    1.41  qed "surjective_sum";
    1.42  
    1.43  goal Sum.thy "R(sum_case f g s) = \